I know a truly marvelous proof of the theorem, which this comment box is too small to contain.

(Seriously, though, I want to know what Fermat’s proof was…Much of the mathematics used in the modern proof was not known in Fermat’s time, so whatever his proof was it was either wrong or stunningly simple.)

A documentary about Andrew Wiles concluded that Fermat was simply mistaken. Although we don’t know the size of the missing proof, “too big for this margin” implies it’s not more than a page long, maybe less. The documentary argued that any such short proof would have been found by now.

But does one human know all the proof? Last year I asked Wiles if he knew all the details of his own proof (30 minutes in), and he does not say “yes”. Indeed he says that he would not want to sit an exam on the proof of Langlands–Tunnell.

I think while the focus on proofs and rigour have certainly helped raise the bar in Mathematics, they are taught and used in many cases where we should be focusing on building an intuition model first, and following with the rigour. One of the reasons why 3brown1blue’s videos are so popular is because he focuses on intuition first, which allows you to get a better handle when you approach the rigour. I understand there are cases where this plain won’t work, but I have seen lots of cases where the Mathematicians don’t even try to explain the intuition and thought behind their models, believing that it is self-evident, when much of the time it isn’t.

Are there any projects focused on building automatic visualizations or explanations of proofs?

Not a general project but I came up with an animated proof of Pythagoras’ Theorem back in the ’90s and recently put together a web page with annotations:

My reading Kevin Buzzard’s concern is that some proofs are enormously complex.
They are based on other proofs that are also enormously complex and very nuanced.
That Andrew Wiles, himself, would have hard time reconstructing his proof and everything the proof relies on, if would be asked to do that as an exam.
Therefore, Kevin, perhaps implies, that machine verification of everything Wile’s proof is based on, is necessary.
Otherwise, we are still ‘not 100% certain’.

With that said, many healthy argument about methods of discovery, this argument has a lot of value, because it drives at least a portion of the scientific community to work on the discovery methods themselves, as it own sub-field.

And it calls the ‘consumers’ of the science to recognize and value/fund this sub field, as enthusiastically.

I know a truly marvelous proof of the theorem, which this comment box is too small to contain.

(Seriously, though, I want to know what Fermat’s proof was…Much of the mathematics used in the modern proof was not known in Fermat’s time, so whatever his proof was it was either wrong or stunningly simple.)

almost certainly

bothIt would be funny if he did have a proof using like a compass and straightedge construction or something.

I lean more towards a timeless joke or simply wrong.

A documentary about Andrew Wiles concluded that Fermat was simply mistaken. Although we don’t know the size of the missing proof, “too big for this margin” implies it’s not more than a page long, maybe less. The documentary argued that any such short proof would have been found by now.

Just iterate through all possible page-long proofs and check whether any of them prove the theorem. Easy-peasy!

Exactly! We may want to pick a limited alphabet, though! :)

I think while the focus on proofs and rigour have certainly helped raise the bar in Mathematics, they are taught and used in many cases where we should be focusing on building an intuition model first, and following with the rigour. One of the reasons why 3brown1blue’s videos are so popular is because he focuses on intuition first, which allows you to get a better handle when you approach the rigour. I understand there are cases where this plain won’t work, but I have seen lots of cases where the Mathematicians don’t even try to explain the intuition and thought behind their models, believing that it is self-evident, when much of the time it

isn’t.Are there any projects focused on building automatic visualizations or explanations of proofs?

Not a general project but I came up with an animated proof of Pythagoras’ Theorem back in the ’90s and recently put together a web page with annotations:

https://seph.github.io/

BTW I struggle with 3brown1blue’s presentations. Maybe I’m not trying hard enough.

I found 3brown1blue’s linear algebra visualizations immensely useful for learning that subject, maybe it was the specific video or topic he covered.

Thank you. I’ll give them a try.

@nesh, thx for posting the original opinion piece, rather than a horribly-worded/disservice to original author article by Vice (discussed here: https://lobste.rs/s/viorkw/number_theorist_fears_all_published_math )

My reading Kevin Buzzard’s concern is that some proofs are enormously complex. They are based on other proofs that are also enormously complex and very nuanced. That Andrew Wiles, himself, would have hard time reconstructing his proof and everything the proof relies on, if would be asked to do that as an exam. Therefore, Kevin, perhaps implies, that machine verification of everything Wile’s proof is based on, is necessary. Otherwise, we are still ‘not 100% certain’.

In my view this is one of the ‘Proving a negative’ arguments ( https://en.wikipedia.org/wiki/Proving_a_negative ) Where his questioning the methods of complex mathematical proofs.

With that said, many healthy argument about methods of discovery, this argument has a lot of value, because it drives at least a portion of the scientific community to work on the discovery methods themselves, as it own sub-field.

And it calls the ‘consumers’ of the science to recognize and value/fund this sub field, as enthusiastically.