> Sounds really cool! Feel free to explain to us how proof
> assistants are going to help out with Economics.
This is exactly what I'm trying to understand. The obvious answer
(or, perhaps, SPEC) is "they'll help in the same way that the help
in mathematics more generally".
Colin, that's what I'm trying to understand myself! I'm doing quite
well, thanks to John and Freek, in using HOL Light to formalize
Hilbert axiomatic geometry. But that's very simple math compared to
what mathematicians normally do, for all that Hilbert geometry is very
poorly understood by mathematicians generally. I'm right now
completely mystified by Tom Hales's much more ambitious use of HOL
Light to formalize his proof of the Kepler conjecture.
I had started looking at HOL due to John's use of it at Intel:
economists use econometric packages, and finance houses use trading
or risk management packages that may contain a lot of infelicities
- JP Morgan, for example, has blamed their recent 'London Whale'
trading losses on change in their VaR ('value at risk') model.
Interesting! May I offer some advice? I read John's thesis (not too
carefully), and it really seemed to me that John's work at Intel
involves John proving actual mathematical theorem for Intel, proofs
involving floating point algorithms that are very hard for humans to
check the correctness of. That sounds like a very valuable
contribution of math to society, but it's not the same as using HOL
Light to check the correctness of a random computer program.
How does VaR and the London Whale compare?
--
Best,
Bill
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
