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.
@johncarlosbaez
> formalization tends to impose consensus
I'm not sure people are getting your point. The way I see it, formalization tends to make people subconsciously think in terms of The One And Only Truth -- and thus consensus.
But we know that in mathematics, there are always other paths, and truths follow from axioms / axiom schemas, which themselves can vary.
Or perhaps I'm missing your point, too.
@dougmerritt - You got my point. Working in Lean or any computer system for formalization, you need to submit to the already laid down approaches, or spend a lot of time rewriting things.
I added a quote from Kevin Buzzard to emphasize the problem:
Kevin Buzzard says "It [formalization? Lean?] forces you to think about mathematics in the right way."
But there's no such thing as "the" right way!
This is just the beginning.
Current systems are the FORTRAN and Pascal of proof systems; they are for building pyramids--imposing, breathtaking, static structures built by armies pushing heavy blocks into place.
What we need is for someone to invent the Lisp of proof systems. Something that helps individuals to think new thoughts.
@maxpool @johncarlosbaez
Yes, well, moving past John's point:
Easier said than done. Current things like Lean are lots better than the systems of years ago, but -- do you have any specific ideas?
I used to follow that area of technology, but I somewhat burned out on it. For now, Terry Tao et al is getting good mileage out of Lean.
I suppose there's some analogy with the period of shift from Peano axioms to ZFC and beyond.
@johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker Somewhat unexpectedly, I find myself on the same side as @xenaproject on this one, I suppose because I read "the right way" differently from @johncarlosbaez
Formalized mathematics makes us think "the right way" in the sense that it requires mental hygiene, it encourages better organization, it invites abstraction, and it demands honesty.
Formalized mathematics does not at all impose "One and Only Truth", nor does it "nail things down with rigidity" or "impose concensus". Those are impressions that an outsider might get by observing how, for the first time, some mathematicians have banded together to produce the largest library of formalized mathematics in history. But let's be honest, it's miniscule.
Even within a single proof assistant, there is a great deal of freedom of exploration of foundations, and there are many different ways to formalize any given topic. Not to mention that having several proof assistants, each peddling its own foundation, has only contributed to plurality of mathematical thought.
Current tools are relatively immature and do indeed steal time from creative thought to some degree, although people who are proficient in their use regularly explore mathematics with proof assistants (for example @MartinEscardo and myself), testifying to their creative potential.
Finally, any fear that Mathlib and Lean will dominate mathematical thought, or even just formalized mathematics, is a hollow one. Mathlib will soon be left in the dust of history, but it will always be remembered as the project that brought formalized mathematics from the fringes of computer science to the mainstream of mathematics.
@andrejbauer @johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
> Mathlib will soon be left in the dust of history
Totally. Even on a technical level, having one dominant math library does not signal the degradation of the field. The other day I learned about [1] for automatically porting Lean definitions to Rocq. This project now gets to start with targeting a big, consistent library of formalized math, and even if the Mathlib people won't care that's still an great thing for the field!
We present lf-lean, a verified translation of all 1,276 statements of the Logical Foundations textbook from Rocq to Lean, produced by frontier AI with ~2 person-days of human effort versus an estimated ~2.75 person-years manually (a 350x speed-up). We achieve this through task-level specification generators: because many software transformations are semantics-preserving, correctness can be defined once for an entire task class and checked automatically across all instances and codebases. This scales human oversight from 𝒪(𝓃) to 𝒪(1) regardless of program complexity. Placed on METR’s time horizon graph, our result suggests verified software engineering is advancing faster than expected.
@mevenlennonbertrand I guess I don't understand their article. I can see how you'd verify that a round-trip Rocq translation is correct (ie. identical) but doesn't that say nothing about the correctness of your Lean code when linked against other Lean code?
Adding to the TCB is not that interesting to me.
@markusde I guess it says that :
- the definitions give you objects which once roundtripped are isomorphic to the original ones ; not the best specification, but rather solid (it rules out everything being unit or something, and is especially fine if you also translate the various operations/basic proofs which encode that they behave the way one expects)
- the lemmas you admit on the Lean side are logically equivalent (up to Lean -> Rocq translation) to ones which are proven, which to me makes them very reasonable to assume
Of course that brings the Lean -> Rocq translation to the TCB, as well as Rocq, but I still feel this is ok?
And I don't see how the liking with other Lean code changes anything, you can treat the translated code as some sort of opaque module with a bunch of definitions and proofs and use that opaquely, just as you would any other Lean module? Except in this one the proofs are not there, they're on the Rocq side
@mevenlennonbertrand I am not comfortable with having that added to the TCB, so, getting back to my initial comment I would not call it "verified" given how easy it is to get wrong! Their article brings up several differences between the Lean and Rocq type theory... can they be sure they caught them all? Apply their technique to a proof development in a different language that is not classically valid. What goes wrong? What if all the definitions they choose to port are round-trippable but some of them are not true????
The answer to this rhetorical question is probably that "they wouldn't trust that" but I think the translation is subtle enough that I wouldn't put faith in it.
John Carlos Baez
DougMerritt (log😅 = 💧log😄)
ma𝕏pool
Andrej Bauer
markusde
Meven Lennon-Bertrand