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 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.
@johncarlosbaez @UweHalfHand Even before computers, a few mathematicians felt that formalization was a good thing to do. Frege, and Russell and Whitehead, are the most obvious examples; Freek Wiedijk also pointed out how similar Euclid's writing is to the input to a proof assistant.
But of course the important question is consent. Mathematicians should be free to build formal proofs, for a variety of reasons. They should never be required to do so
@richardelwes - I don't object to my work being formalized.
I think a lot of people are spending time and money on formalization which they could better spend on something else. I encourage pluralism, so I expect that lots of mathematicians will do things that are not to my taste, including this. But bandwagons tend to decrease pluralism - especially ones where you get "locked in" to a specific software package.
@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 @andrejbauer @pigworker I can give it a try.
First: Lean and Mathlib embody a very particular philosophy. Lean 4 aims to be "practical", which is mainly code for 'allowing lots of automation'. It cuts some serious corners to achieve that (others have written about that at length). Mathlib chooses to be a 'monorepo' (which is laudable indeed IMHO). The combination of Lean's technology choices and the monorepo decision is what forces 'consensus'.
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I would compare Lean+Mathlib to Java rather than FORTRAN and Pascal: Java is just as boring a PL as others, but it is a much stronger ecosystem (IDEs, libraries, tutorials, etc). Thus developers have a much better experience using Lean+Mathlib and the surrounding ecosystem (blueprints are super cool, as just one example).
In my mind, it is purely 'social forces' that has made and is making Lean+Mathlib the apparent winner. And that has snowballed - almost to the point of smothering everything else, which is extremely dangerous for innovation.
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker Are there specific ideas around to make things better? Absolutely! Heck, there are old ideas (Epigram comes to mind, but even Automath has not been fully mined yet) that are still not implemented.
I will continue later - need to attend to other things right now.
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker On the more optimistic side:
To me, what's really missing are experts in designing UX having a solid look at mechanized mathematics tools. For that to bear fruit, experts in requirements analysis need to better understand the full "mathematics workflow" -- where proof is just one small aspect. It might indeed be the most time-consuming part, but it is not necessarily where the most value lies. [See LaTeX as an example of a strong value proposition that has completely changed the practice of mathematics, but in a surreptitious way, as it is essentially invisible wrt "mathematical thought". Its effect is no less important.]
@sandmouth @JacquesC2 @johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I mean... I'm serious about it. I've seen really convincing arguments from type theorists about how Lean's type theory is missing features (transitive defeq, decidable defeq, consistency with various axioms). Some of the missing features are just mistakes, but some of them are made in the interest of usability or simplicity or speed or whatnot.
Personally, I don't think has decisively shown that these things _aren't_ in conflict, so that is the sense in which I see Lean as worse and better. Idk, just my opinion.
@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.
@andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
It is not inconceivable that one day in the not-too-distant future, proof assistants will be able to "understand" proofs written in sufficiently careful, informal, mathematical vernacular and translate it to a suitable formal language.
And this formal language doesn't need to be fixed. The mathematician just chooses a foundation, or, in case they don't care, they let the proof assistant choose a suitable one for the informal (but hopefully rigorous) mathematics at hand.
I don't mean AI, but people are certainly trying this with so-called AI nowadays (personally, I think this is the wrong approach, but **I don't want** this to become the subject of discussion here).
In any case, a person will need to check that the definitions and the statements of the theorems and constructions are correctly translated (*). Then the formal proofs obtained from informal proofs don't need to be checked by people.
(*) At least at the beginning. For example, we now trust that C compilers produce correct machine code and don't check it ourselves.
In any case, all of the above can happen only step by step, and currently we are at an important step, I think, where the first were in the 1960's by de Bruijn.
As I said before, I use proof assistants as smart blackboards. If I could get interactive help while I write in mathematical vernacular, I would immediately adopt this incredible new proof assistant.
And, I repeat, I don't mean the kind of non-help I get from ChatGPT, Gemini, Claude, DeepSeek, or what-you-have - I feel I help them rather than the other way round.
I mean the kind of help I already get in non-AI-based proof assistants
@andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
And let's not forget.
Everybody here and elsewhere says Lean, Lean, Lean.
Before Lean, we have a long list of successful proof assistants.
In particular, Lean is based on both Rocq (formerly known as Coq) *and* the foundations of Rocq, namely the "calculus of inductive constructions".
Lean is Rocq with a new skin and a new community, based on the very same foundations and approaches.
I can say this without any conflict of interest, because I prefer Agda instead, which is based on a different foundation, namely MLTT.
And this preference is based on the kind of mathematics *I* prefer (constructive, suitable for being interpreted in any (infinity) topos, in the (in)formal language of HoTT/UF).
@MartinEscardo @andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
while I mostly agree, I think Lean also inherits many ideas from Isabelle, not about foundations at all but instead about things like proof search and automation.
@MartinEscardo @andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
It seems to me that anything that translates careful but informal mathematical vernacular into a formal language, must ipso facto be AI. But that doesn't mean that it would be the kind of AI that you describe as unhelpful at the end of your post. Rather, it means that AI encompasses much more than those things.
@TobyBartels It is interesting you say this.
Some things that were considered AI in the past are now deterministic algorithms.
For example, checking formal proofs with incomplete information (to be reconstructed by the checker) for correctness.
@andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
@MartinEscardo @andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
It's strange to read about the history of the MIT AI Lab and all of the things that they developed that don't (or no longer) seem like AI. Maybe just as philosophy is the study of ideas that have not yet matured enough to become science, so AI is the study of programming methods that have not yet matured. So even if this transition work is technically done by a large language model similar to the ones that you mentioned, your hope is that it won't be AI anymore so it won't be slop.
@andrejbauer - "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."
I did read it differently. I was really worrying that Kevin meant formalizing mathematics in *Lean* forces us to think the right way. But in fact I don't think formalizing mathematics at all makes us think "the" right way. It has good sides, which you mention, so it's *a* right way to do mathematics. But it also has bad sides. Mostly, it doesn't encourage radical new ideas that don't fit well in existing formalisms. Newton, Euler, Dirac, Feynman and Witten are just a few of the most prominent people who broke out of existing frameworks, didn't think formally, and did work that led to a huge growth of mathematics. If you say "those people are physicists, not mathematicians", then you're slicing disciplines differently than me. I find their ideas more mathematically interesting than most mathematics that fits into existing frameworks.
@dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
I don't agree that working with a proof assistant will reduce the chance that we'll come up with radical new ideas.
It's not at all difficult for me to picture someone like Grothendieck, who also broke out of many existing formalisms, writing his own library from scratch in order to express his ideas -- In many ways this is exactly what he did! Though of course he (and his collaborators) wrote a long series of books rather than writing a long list of agda/lean/etc files.
In fact, it's quite easy for me to picture someone like Grothendieck writing their own theorem prover! Perhaps in that world EGA/SGA would look much more like the currently-under-development synthetic algebraic geometry, formalized in a proof assistant that's custom made for arguments in the (big) zariski or etale topos.
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
It is not clear who specifically you are replying to. I hope it is not me.
@johncarlosbaez @andrejbauer @dougmerritt @JacquesC2 @pigworker @xenaproject
Sorry, let me adopt your convention to make my reply more clear -- but you can tell I was replying to John since it's his post that show up above mine when you click my post (at least on my instance)
@johncarlosbaez @andrejbauer @dougmerritt @JacquesC2 @pigworker @xenaproject
@hallasurvivor - I don't think Grothendieck broke out of existing formalisms in quite the way I'm talking about. Though it broke radically new ground, all his work was rigorized very quickly. The people I mentioned did work that either took a century or more to make rigorous, or is still in process of being brought into the fold of rigorous mathematics. I'm talking about Newton's calculus, Euler's manipulations of divergent series to compute the zeta function, Feynman's path integrals, and the many path integral "proofs" given by Witten.
There are dozens of less famous but still interesting examples. I would never have written a paper about the Cobordism Hypothesis (and the still less finished Tangle Hypothesis and Generalized Tangle Hypothesis) if I had been thinking about formal definitions or proofs.
(That's an example that comes from outside analysis! But my other examples suggest analysis is a lot more future-leaning than algebra, in the sense of racking up debts against future formalization.)
@johncarlosbaez
the hyperreals are so "easy" to formalize its hard to imagine how long we went without a formalism.
What's also interesting is how strong the pushback is about NSA. Multiple times a week on the internet calculus students will ask questions about dy/dx being a fraction or not... mention nonstandard analysis and youre likely to get down voted and attacked as unhelpful... happens on r/learnmath regularly.
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
@johncarlosbaez writes "But in fact I don't think formalizing mathematics at all makes us think the right way."
You should try it once to see by yourself. You are talking about something you've never done.
I say this because I also said the same thing as you said in the past.
And here is the first time I repent in public:
Computing an integer using a Grothendieck topos
https://math.andrej.com/2021/05/18/computing-an-integer-using-a-sheaf-topos/
@andrejbauer @dougmerritt @JacquesC2 @pigworker @xenaproject
@MartinEscardo - how long would it take to "try it once"? Then I can weigh that against other things I could do with that time.
I have absolutely nothing I want to formalize, and I'd be weighing time spent on this against things like learning how to make music on a digital audio workstation, which I put off because it doesn't provide the instant gratification of playing a piano, but which I know I'd like in the end. In either case I know I'll start by suffering for hours, learning someone else's syntax and conventions instead of thinking my own thoughts. But for music software I know I'll eventually get a product I enjoy that I couldn't make any other eay.
Have a look at these Lean games:
It's good to work a few examples to see how they spell out in a proof assistant. It's not difficult! It's fun!
I see proof assistants as a sort of calculator for assumptions. They really shine when you throw lots of stuff at them, like verifying computer programs. Which involves lots of boring stuff, and a proof assistant can help with that! If it's a burden then don't use a proof assistant.
yen
John Carlos Baez
Conor Titania Mc Bride
Liu Yao εζ³
Strider Uwe πΊπ¦π¨π¦π²π½
Richard Elwes
DougMerritt (logπ
= π§logπ)
maπpool
Jacques Carette
markusde
Philip Zucker
Andrej Bauer
Meven Lennon-Bertrand
leonardo m.
Martin Escardo
Liam O'Connor
The Blue Wizard
TobyBartels
Christina Grossack
Daniel Lakeland
Boyd Stephen Smith Jr.
Refurio Anachro