4 ms·

Last week Microsoft Research posted an interesting talk by Kevin Buzzard [1] from Imperial College London about how he wants to formalize all mathematics with t

Last week Microsoft Research posted an interesting talk by Kevin Buzzard [1] from Imperial College London about how he wants to formalize all mathematics with theorem provers. He's currently using LEAN [2]. Half of the talk is a discussion of the challenges he's faced convincing other mathematicians that this is valuable, and the other half is about his success using LEAN as a tool to teach undergraduates about formal proofs in general. I think Alloy was mentioned at the end, but not really compared to LEAN. [1]: https://youtu.be/Dp-mQ3HxgDE https://youtu.be/Dp-mQ3HxgDE [2]: https://leanprover.github.io/ https://leanprover.github.io/

dnpp123 7y ago
Isn't it the same thing that guys at INRIA with COQ are trying to do since ages ?
dang 7y ago
Discussed on HN the other day: https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721. Also a month ago: https://news.ycombinator.com/item?id=20909404 https://news.ycombinator.com/item?id=20909404 It's an excellent talk. I couldn't stop watching it.
nickpsecurity 7y ago
Convincing mathematicians about it is a really old problem. Here's the first paper I saw really describing how mathematics has been done as a social process focused on people's understanding: https://www.cs.cmu.edu/~pattis/misc/socialproofs.pdf https://www.cs.cmu.edu/~pattis/misc/socialproofs.pdf A 2009 rebuttal to be fair to my side of the debate: https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=400A0F7C050239C990098177E0C7FBA8?doi=10.1.1.150.4680&rep=rep1&type=pdf https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=40... Here's a recent article about the situation from yet another segment of people trying to bring in automation: https://www.quantamagazine.org/in-computers-we-trust-20130222/ https://www.quantamagazine.org/in-computers-we-trust-2013022... Unlike article's impression, a lot of how to build trustworthy provers has already been solved. The state-of-the-art is probably Milawa: a prover for ACL2-like logic running on a Lisp verified down to the machine code. It has summaries of various approaches of making computational math/logic trustworthy: https://www.kookamara.com/jared/2015-jar-milawa.pdf https://www.kookamara.com/jared/2015-jar-milawa.pdf Note: Like in Common Criteria EAL7 or DO-178C, I'd use a mix of techniques for verification instead of blindly trusting the math. Lots of human review, static analysis, testing, etc. Far as projects implementing math's foundations, you should especially check out Mizar (most complete) and Metamath (open source): https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Metamath https://en.wikipedia.org/wiki/Metamath If authors give permission, it might be worthwhile to attempt to create re-writing tools that convert those tools languages into platforms in use by programmers. That's mainly Coq, the HOL's, Why3, and (hardware) ACL2. I don't know how feasible that is. I just think it could be valuable.

dnpp123 7y ago

Isn't it the same thing that guys at INRIA with COQ are trying to do since ages ?

dang 7y ago

Discussed on HN the other day: https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721. Also a month ago: https://news.ycombinator.com/item?id=20909404 https://news.ycombinator.com/item?id=20909404 It's an excellent talk. I couldn't stop watching it.

nickpsecurity 7y ago

Convincing mathematicians about it is a really old problem. Here's the first paper I saw really describing how mathematics has been done as a social process focused on people's understanding: https://www.cs.cmu.edu/~pattis/misc/socialproofs.pdf https://www.cs.cmu.edu/~pattis/misc/socialproofs.pdf A 2009 rebuttal to be fair to my side of the debate: https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=400A0F7C050239C990098177E0C7FBA8?doi=10.1.1.150.4680&rep=rep1&type=pdf https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=40... Here's a recent article about the situation from yet another segment of people trying to bring in automation: https://www.quantamagazine.org/in-computers-we-trust-20130222/ https://www.quantamagazine.org/in-computers-we-trust-2013022... Unlike article's impression, a lot of how to build trustworthy provers has already been solved. The state-of-the-art is probably Milawa: a prover for ACL2-like logic running on a Lisp verified down to the machine code. It has summaries of various approaches of making computational math/logic trustworthy: https://www.kookamara.com/jared/2015-jar-milawa.pdf https://www.kookamara.com/jared/2015-jar-milawa.pdf Note: Like in Common Criteria EAL7 or DO-178C, I'd use a mix of techniques for verification instead of blindly trusting the math. Lots of human review, static analysis, testing, etc. Far as projects implementing math's foundations, you should especially check out Mizar (most complete) and Metamath (open source): https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Metamath https://en.wikipedia.org/wiki/Metamath If authors give permission, it might be worthwhile to attempt to create re-writing tools that convert those tools languages into platforms in use by programmers. That's mainly Coq, the HOL's, Why3, and (hardware) ACL2. I don't know how feasible that is. I just think it could be valuable.