quanta article

Stream: general

[Reid Barton]

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]

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]

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]

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

Yeah, I have no idea

[William Whistler]

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

[William Whistler]

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

[Kevin Buzzard]

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]

@Kevin Buzzard Will they be streamed/recorded?

[Kevin Buzzard]

No idea! I could ask.

[Floris van Doorn]

How did the debate go? Was it recorded?

[Kevin Buzzard]

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.