How Math’s Most Famous Proof Nearly Broke (2015) | Hacker News Reader

How Math’s Most Famous Proof Nearly Broke (2015)

nautil.us

102 pointsdnetesn42 comments

I can recommend Simon Singh's book on this topic, his writing is rather captivating (The Big Bang is one of the best books I've read, so is the Code Book). He also made a BBC documentary on the topic.

https://simonsingh.net/books/fermats-last-theorem/

I'd also recommend his The Code Book - https://simonsingh.net/books/the-code-book/

Nice easy reading on the history of codes.

+1 for the movie. It used to be on youtube but I can't find it right now. Perhaps the BBC had it removed. This is the finest moment in the movie, for me, when Wiles describes the moment when everything clicked. The whole movie is well worth watching.

https://www.youtube.com/watch?v=SccDUpIPXM0

Look at Vimeo instead.

I also want to urge anyone with even just a fleeting interest in mathematical topics like this to go out looking for said BBC documentary. It's a marvelous portrait of the characters and backstories behind this proof.

It is a good book but the last chapter is a rush.

Is it really fair to say that Wiles proof is the most famous in mathematics? Seems to me like something like the Euclid’s proof of the infinitude of the primes might be more well known? Or the standard geometrical proof of Pythagoras theorem?

It’s certainly true that far more people understand and know how to prove the infinitude of the primes than understand/know how to prove Wiles’ proof. Wiles’ result has received far more press coverage in the last 30 yeas though. In this sense it is more famous.

An amazing (word of a number theorist) documentary from the BBC's Horizon program: https://www.dailymotion.com/video/x223gx8 You can see Wiles crying when he talks about his work.

This brings up a question I have. Is there a way we can code up proofs in a computer language and have it checked for correctness? If so, how? What resources can I follow up on? Can current technologies check really complicated proofs like this one?

This is not as easy as some comments here imply. Basically, there are 3 popular languages used for this in a academia and the industry: Coq, Isabelle/HOL and Agda. They're all extremely different languages doing different things (but their end goal is the same: formalizing and automating proving). Coq and Agda are intuitionistic by design, you need assume lem to be classical. Agda has a Haskell heritage so it's purely functional other two are more "procedural". Coq has 2 languages built into it, a tactic language and a language go write types in.

Anyway this is one of the hottest research topics in CS. I know we keep seeing deep learning papers all the time, one might think this is the only thing happening in CS world. Currently it is nowhere near easy to formalize a complex enough theorem in a system like this. Good news is there is a large chunk of certain theories (like homotopy theory) already formalized for you, so you can go ahead and use them as libraries.

The biggest challenge is mathematics is written for humans, it is not meant to be formal. When you formalize theorems you start proving smallest shit you'd never have thought that would need a proof. You even need to prove things like what it means x == y and that for all x, x==x. There is no AI involved in this currently, so it's a very manual, intellectually complicated and long process. These systems have a proof finder built into them which performs a tree search with heuristic to help you, this usually makes manual proofs easier, but usually only marginally easier and you still have to micromanage your proofs.

Keywords you can search: automated theorem proving, dependent type theory and homotopy type theory.

To be clear though, all the mentioned languages are built on purely functional programming. Coq and Isabelle are more "procedural" in that they include special proof languages that express proofs in a step-by-step way that feels procedural, but the programs and definitions one proves properties of are still expressed in a functional style.

It's true that one needs to prove a lot of trivial things in all these systems, but the extent of this varies dramatically based on how much automation they provide. For example, Agda includes only minimal, barebones proof automation, while both Isabelle and Coq allow using more sophisticated automation that can take care of a lot of trivial steps automatically (such as "x == x").

> they include special proof languages that express proofs in a step-by-step way that feels procedural

Serious proof developments don't even use the languages in a procedural way. They use "declarative" idioms/patterns that are structured more like a very detailed human proof. This is because "procedural" interaction with the proof state is extremely fragile (it's like raw assembly code, the slightest change in any part of the proof can break basically everything else in it) plus it actually requires "replaying" the proof in order to have any chance of understanding how it works. Declarative idioms can be read and understood directly, at least to some extent.

Voevodsky developed Univalent Foundations in order to catch subtle mistakes in his (and others) result:

"Only then did I discover that the proof of a key lemma in my paper contained a mistake and that the lemma, as stated, could not be salvaged. Fortunately, I was able to prove a weaker and more complicated lemma, which turned out to be sufficient for all applications. A corrected sequence of arguments was published in 2006.

This story got me scared. Starting from 1993, multiple groups of mathematicians studied my paper at seminars and used it in their work and none of them noticed the mistake. And it clearly was not an accident."

More details on page 8 in the IAS newsletter article

https://www.ias.edu/sites/default/files/pdfs/publications/le...

There is also a Quanta article:

https://www.quantamagazine.org/univalent-foundations-redefin...

This is interesting. What are the prerequisites to understand Univalent Foundations and how active is it?

Look into the Coq language, it is under active development and there is a lot of work going into it. Voevodsky was working in Coq, if I recall.

As to how hard it is to learn, you will have to learn a pretty decent amount. It all depends on your background. If you know what the Curry Howard correspondence is, you are in relatively good shape. If you've never heard of lambda calculus or first order logic, you may have some more work cut out for you.

Here is a nice article I read last night on explaining the move from set theory to type theory. It gets a bit technical but you might be able to get something from it.

https://golem.ph.utexas.edu/category/2013/01/from_set_theory...

If you're specifically interested in Univalent Foundations, just read the book. https://homotopytypetheory.org/book/

In addition to Coq that other commenters mentioned, there is also a family of proof assistants based on higher-order logic. Isabelle/HOL[1] is probably the most widely used prover in this family, which also provides a great deal of automation compared to other provers. For example, it has been used to verify the seL4 microkernel [2]. As for introductions to the topic, I can recommend "Concrete Semantics" [3] which introduces the reader to Isabelle/HOL generally and shows how to model semantics of programming language and prove properties about them.

For Coq, a widely used book to get started is Software Foundations [4] which is also focused on PL semantics.

[1] https://isabelle.in.tum.de/

[2] https://sel4.systems/

[3] http://www.concrete-semantics.org/

[4] https://softwarefoundations.cis.upenn.edu/

Yes! There are several different languages and systems used for coding proofs. Coq [1] is probably the most well known. But, as you alluded to, it is not convenient (or easy) to code all proofs in such a style.

1. https://coq.inria.fr/

At OPLSS 14, Andrew Appel characterized programming in Coq as the world's best video game, I would have to say it's a close second.

I recall it was accessible if you had programmed in an ML, start here: https://softwarefoundations.cis.upenn.edu/

Isabelle[1], Coq[2], and Metamath[3] are probably the three most well-known automated proof assistants but there are many others[4]. Using them is very similar to programming - the mathematician writes his proof in a formal language using a text editor or IDE, and a "compiler" either verifies the proof or produces error messages. Most of these also have features which "assist" the author by automatically searching for formal steps to fill in the gaps between what the author wrote. They also provide libraries/modules/packages for topics like number theory, geometry, calculus, etc., so that you can build off of standard definitions and well-known theorems instead of starting from scratch.

Of these, Isabelle and Coq compete for best-of-breed and are extremely powerful. Metamath on the other hand is intentionally minimalist, starting at a level below logic (string substitution rules, basically) and building up predict logic inside the system. Metamath comes with a "proof explorer"[5] - an online body of proofs formally verified by metamath.

For proofs about algorithms in particular, TLA+ [6] is a formal specification language which can prove things about algorithms, as charmingly described in "Euclid Writes an Algorithm."[7]

[1]: https://isabelle.in.tum.de/ [2]: https://coq.inria.fr/ [3]: http://us.metamath.org/ [4]: https://en.wikipedia.org/wiki/Proof_assistant [5]: http://us.metamath.org/mpeuni/mmset.html [6]: https://learntla.com/introduction/ [7]: https://lamport.azurewebsites.net/pubs/euclid.pdf

Another approach would be: https://www.manning.com/books/type-driven-development-with-i...

If you are a programmer who hasn't touched any functional programming, this would probably blow your mind all over the place.

I've been curious about Idris, but apparently there was recently an amazing talk from an (the?) Idris creator talking about rewriting it from scratch with a major emphasis on relying on linear logic. He demonstrated how it does a lot of proving work for you automatically, which caused a lot of wows and applause. Anyway, I'm not sure how valuable it will be for me to learn the current version of Idris given that.

https://leanprover.github.io/

LEAN has significant momentum right now. I was at the International Congress of Mathematical Software this summer (as a plenary speaker), and the other plenary was about LEAN, as were a bunch of talks. There are also excellent VSCode, Emacs, and CoCalc modes for using LEAN. The Zulip LEAN chat channel (https://leanprover.zulipchat.com/) is also very active.

How does LEAN compare to Coq/Isabelle/Agda?

I know Coq exists but that's about it https://coq.inria.fr/

This is how my discrete logic class in college was taught. To code the proofs, we used Haskell.

That was quite an enjoyable read.

It's so interesting that a problem so simple to explain would require hundreds of pages of proof.

I'm really interested in whether the Collatz conjecture will be proven too.

Maybe you'll like this FLT related story too, it's the most worthwhile numberphile video:

https://m.youtube.com/watch?v=nUN4NDVIfVI

What are the practical ramifications of FLT? It sounds like there may be crypto implications w elliptical curves.

As the article said, none really. It's more the tools that were created to solve it that are useful. FLT is like the Apollo mission of Mathematics and has been for hundreds of years. A crazy dream of no direct immediate practical value, but the pursuit of which sparks innovation and dreams.

What's interesting about FLT is that in the sense of proving a hypothesis, although the attempts themselves have lead to failures in their objective, they often illuminated whole new areas of mathematics, but this realization only comes somewhat later than when the proof is realized. It was obvious that a particular attempt had failed relatively quickly, but the lessons learned and their applications required a keen (creative mathematical) eye to spot.

Badiou (a continental political philosopher interested in the philosophy of mathematics) uses FLT as an example in political contexts, to what extent we can say that a utopian vision has failed even if it results in disaster, we should be (and some have been) looking out for the lessons which are learned after failure.

That last sentence about Badiou, whoever that is, was a sharp turn to the left.

Human as an individual is not a number. Yes may be for the philosopher king for an ideal which not everyone agree or vote for may or may not come or forever waiting, we just kill millions and millions.

Maos has it and starve 30 millions.

Soviet Union.

USA has its Vietnam and 2nd Iraq war.

I am not saying we should not try but Great Saint begot Great Thief. Be afraid of people who sit in their arm chair and talk about scarifie for the ideal.

Interesting read. Wikipedia recounts the tale as well - https://en.wikipedia.org/w/index.php?title=Fermat%27s_Last_T...

A 200 page proof even if it is correct may not be the most elegant proof for this problem since Fermat noted that his proof was too long to fit on the margin. This suggests at most a one page proof.

Also I'm curious if it can be proved that only one proof is possible. There are several independent proofs of the Pythagoras theorem.

Fermat could have been mistaken about his proof, however.

That's a possibility. But I still think there must be a more direct proof. A shorter proof that can be understood by anyone who is familiar with Euclid. I believe a proof by using only mathematical methods known to Fermat must be possible.

You can make any proof as short as you want. Length of proof means almost nothing; it is a function of the language you choose to use.

> You can make any proof as short as you want.

If so why did Wiley choose to write a 200 page proof while he could have stated it in one sentence?

Because he was writing for a specific class of predetermined parsers, rather than an arbitrary one which was optimized for his proof.

Reply on news.ycombinator.com