Fermat's last theorem puzzled mathematicians for centuries until it was finally proven in 1993. Now, researchers want to create a version of the proof that can be formally checked by a computer for any errors in logic
They're using Lean for the proofing for those interested. It's a pretty neat system from the little I've seen. Uses a graph to represent the proof path and pre-requisites, and it's kinda integrated with TeX.
They're using Lean for the proofing for those interested. It's a pretty neat system from the little I've seen. Uses a graph to represent the proof path and pre-requisites, and it's kinda integrated with TeX.
Terence Tao talks about it here
I found a YouTube link in your comment. Here are links to the same video on alternative frontends that protect your privacy: