Zulip Chat Archive

Stream: general

Topic: quanta article


Reid Barton (Jun 03 2019 at 17:07):

Quanta magazine article about formalized mathematics and FLT: https://www.quantamagazine.org/why-the-proof-of-fermats-last-theorem-doesnt-need-to-be-enhanced-20190603/

Jesse Michael Han (Jun 03 2019 at 17:37):

I was reminded of this unexpectedly in 2017 when, in the space of a few days, two logicians, speaking on two continents, alluded to ways of enhancing the proof of FLT — and reported how surprised some of their colleagues were that number theorists showed no interest in their ideas.

I wonder who these "two logicians" are...

Johan Commelin (Jun 03 2019 at 17:52):

But — unlike many who follow number theory at a distance — they were certainly aware that a proof like the one Wiles published is not meant to be treated as a self-contained artifact. On the contrary, Wiles’ proof is the point of departure for an open-ended dialogue that is too elusive and alive to be limited by foundational constraints that are alien to the subject matter.

@MichaelHarris can't we have both? Both the self-contained watermark-stamped artifact, and the point of departure for an open-ended dialogue?

Reid Barton (Jun 03 2019 at 17:52):

I wonder who these "two logicians" are...

Yeah, I have no idea

William Whistler (Jun 03 2019 at 18:03):

I would guess Colin McLarty for one: https://mathdept.ucr.edu/research/Col_4-12-2017.pdf

William Whistler (Jun 03 2019 at 18:03):

https://en.wikipedia.org/wiki/Colin_McLarty

Kevin Buzzard (Jun 03 2019 at 18:58):

You know there's a big bout between Michael Harris (representing old skool mathematics) and Patrick and I (representing Lean) in Paris on 20th June: https://mdetlefsen.nd.edu/philmath-intersem/philmath-intersem-10-2019/ . Note also Silvia De Toffoli on 6th (she was one of the philosophers who spoke at Big Proof).

I've asked lots of number theorists (including Taylor) whether they would be interested in seeing a formal proof of FLT and they were all completely indifferent. I've also asked lots of number theorists (including Wiles!) whether they understand all of the proof, and they've all said no. It's an interesting phenomenon.

William Whistler (Jun 03 2019 at 19:02):

@Kevin Buzzard Will they be streamed/recorded?

Kevin Buzzard (Jun 04 2019 at 06:39):

No idea! I could ask.

Floris van Doorn (Jun 20 2019 at 23:47):

How did the debate go? Was it recorded?

Kevin Buzzard (Jun 21 2019 at 06:20):

It was not recorded. It was interesting. I gave my usual paranoid spiel about how maths was full of holes and an audience member (called David something -- Patrick do you know who that guy was?), a historian, said that maths has always been like that. We talked about whether it was possible to measure whether it was getting worse, but this is complicated by the fact that the size of gaps can change as people develop new techniques.

Michael represented a position at the opposite extreme to me, arguing that his papers were just stories/dialogues, and he was not claiming to prove anything. Patrick demonstrated Lean to a room of philosophers :-) and argued that thinking about things the way lean forces you to is good for mathematics because it makes your proofs better.


Last updated: Dec 20 2023 at 11:08 UTC