Fermat's Last Theorem – how it’s going
xenaproject.wordpress.com
Fermat's Last Theorem – how it’s going
1–10 of 216 posts
Re: Fermat's Last Theorem – how it’s going
#2[flagged]
Re: Fermat's Last Theorem – how it’s going
#3> Lean did that irritating thing which it sometimes does: it complained about the human presentation of an argument in the standard literature, and on closer inspection it turned out that the human argument left something to be desired.
Tongue-in-cheek irritation aside, this is actually awesome. I think Lean (and other theorem provers) are going to end up being important tools in math going forward.
Re: Fermat's Last Theorem – how it’s going
#4I’m happy to see so much work going into fixing human errors in mathematics in a rigorous way.
Re: Fermat's Last Theorem – how it’s going
#5> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the experts” but not correctly documented. The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. For me, this is just one of many reasons why humans might want to consider getting mathematics written down properly, i.e. in a formal system, where the chances of error are orders of magnitude smaller. However most mathematicians are not formalists, and for those people I need to justify my work in a different way. For those mathematicians, I argue that teaching machines our arguments is a crucial step towards getting machines to do it themselves. Until then, we seemed to be doomed to fix up human errors manually.
It makes me think about how you get UI/UX/web designers who make (informal, imprecise) mockups and prototypes of their design ideas and interaction flows, they then hand these off to a developer to do the coding (formalise it, explain it precisely to the machine), and on the way the developer will inevitably find problems/holes in the designs (like an interaction scenario or code path not considered in the design, which could uncover a major design flaw), which the developer and/or the designer will have to patch somehow.
As in, design and development are different roles and require different mindsets, and most designers have a very strong resistance against working and thinking like a developer.
Re: Fermat's Last Theorem – how it’s going
#6> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the experts” but not correctly documented. The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. For me, this is just…
> consider getting mathematics written down properly, i.e. in a formal system
This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.
Re: Fermat's Last Theorem – how it’s going
#7This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha.
Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.
Re: Fermat's Last Theorem – how it’s going
#8> Lean did that irritating thing which it sometimes does: it complained about the human presentation of an argument in the standard literature, and on closer inspection it turned out that the human argument left something to be desired. Tongue-in-cheek irritation aside, this is actually awesome. I think Lean (and other theorem provers) are going to end up being important tools in math going forward.
Compilers have this very same habit!
Re: Fermat's Last Theorem – how it’s going
#9If you're interested in this stuff at all, check out some code.
Example: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
Also check out the blueprint, which describes the overall structure of the code:
https://imperialcollegelondon.github.io/FLT/blueprint/
I'm very much an outside observer, but it is super interesting to see what Lean code looks like and how people contribute to it. Great thing is that there's no need for unittests (or, in some sense, the final proof statement is the unittest) :P
Re: Fermat's Last Theorem – how it’s going
#10> Lean did that irritating thing which it sometimes does: it complained about the human presentation of an argument in the standard literature, and on closer inspection it turned out that the human argument left something to be desired. Tongue-in-cheek irritation aside, this is actually awesome. I think Lean (and other theorem provers) are going to end up being important tools in math going forward.
Compilers have this very same habit!
Yes. In fact, Lean is a compiler and type checkers are theorem provers (by the Curry-Howard correspondence). Proofs are programs!