3 ms·

> formalizing mathematics currently seems far too much work to be worth the time of the working mathematician A very general statement that isn’t true in all c

> formalizing mathematics currently seems far too much work to be worth the time of the working mathematician A very general statement that isn’t true in all cases. I recommend taking a look at the LEAN mathlib project. It is a group of working mathematicians proving leading edge mathematics correct using a formal proof tool (LEAN). The problem with leading edge mathematics seems to be that the proofs are too complex for anybody but a few specialists to verify the traditional way. And those specialists are already busy working on their own proofs. So having an automated assistant verifying the proofs seems to be necessary for the future of mathematics. I am not a working mathematician myself however that is the impression I am getting reading articles written by leading edge working mathematicians. The same way that large complex software applications are too complex for humans to verify without the help of automated proof tools.

fspeech 4y ago
When Hales started in 2003 the Flyspeck project https://github.com/flyspeck/flyspeck https://github.com/flyspeck/flyspeck to formally verify his own proof of the Kepler conjecture he likely didn't know that it would take him (and a team of helpers later) until 2014 to finish. He used hol-light, which is very much geared towards proof automation. Lean is more expressive (being dependently typed) but I am not aware of any real advance in automation over hol-light. Indeed with their focus on code generation (therefore constructive logic) and software verification, proof automation for math is likely harder in Lean. But the expressiveness and good tooling seem to have generated a lot of interests and mathlib has a real active community, which is really good to see.
- mbrodersen 4y ago
  Yep agree. Having an active team of working mathematicians and field medalists giving feedback to the LEAN development team is really helpful in pushing automation forward. Having said that, for people like me, who doesn’t care about formalising mathematics but do care about proving code correct, proof automation has already come a long way and is on the edge of becoming a practical tool for highly critical software.

fspeech 4y ago

When Hales started in 2003 the Flyspeck project https://github.com/flyspeck/flyspeck https://github.com/flyspeck/flyspeck to formally verify his own proof of the Kepler conjecture he likely didn't know that it would take him (and a team of helpers later) until 2014 to finish. He used hol-light, which is very much geared towards proof automation. Lean is more expressive (being dependently typed) but I am not aware of any real advance in automation over hol-light. Indeed with their focus on code generation (therefore constructive logic) and software verification, proof automation for math is likely harder in Lean. But the expressiveness and good tooling seem to have generated a lot of interests and mathlib has a real active community, which is really good to see.

mbrodersen 4y ago
Yep agree. Having an active team of working mathematicians and field medalists giving feedback to the LEAN development team is really helpful in pushing automation forward. Having said that, for people like me, who doesn’t care about formalising mathematics but do care about proving code correct, proof automation has already come a long way and is on the edge of becoming a practical tool for highly critical software.