John Carlos BaezMar 29

I don't want to formalize any of my work on mathematics. First because, as Emily Riehl notes, formalization tends to impose consensus. And second, because I find it boring. It steals time from creative thought to nail things down with more rigidity than I need or want.

Kevin Buzzard says "It forces you to think about mathematics in the right way." But there is no such thing as "the" right way to think about mathematics - and certainly not one that can be forced on us.

https://www.quantamagazine.org/in-math-rigor-is-vital-but-are-digitized-proofs-taking-it-too-far-20260325/

In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far? | Quanta Magazine

The quest to make mathematics rigorous has a long and spotty history — one mathematicians can learn from as they push to formalize everything in the computer program Lean.

Quanta Magazine
Show threadConor Titania Mc BrideMar 29
@johncarlosbaez haha! if you happen to work in the formalisation industry, you're routinely reassured by how little consensus there actually is.
Show threadJohn Carlos BaezMar 29
@pigworker - Good! But to get anywhere with formalizing big theorems in Lean, the topic mainly discussed in this article, you're pressured to work within that system.
Show threadConor Titania Mc BrideMar 29
@johncarlosbaez Aye! It's depressing to see these tools flip to being the new orthodoxy in no time flat. I'm both impressed and depressed by Lean. I think we can do better, but we may not be allowed to.
Show threadConor Titania Mc BrideMar 29
@johncarlosbaez And yes, ownership of "the right way" is a political project which need not lie at the heart of this innovation, but apparently does.
Show threadJohn Carlos Baez
@pigworker - Elsevier must already be drooling, thinking of a future where you need to formalize your theorems to publish them... and you need to formalize them in a system owned by Elsevier. We're not there yet, but formal systems of math always have "economies of scale" that foster conformity, and once everyone is using Lean, someone will figure out a way to charge for it.
Mar 29 at 8:45pmWeb
Show threadConor Titania Mc BrideMar 29

@johncarlosbaez And the ACM are very nearly there!

The thing is that to have any credibility, the proof rules need to be open and the checking procedure needs to be independently reimplementable.

Lean's is. And it's broken, but not in a way that says yes to wrong things.