@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!

@johncarlosbaez @dougmerritt

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 - "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

@johncarlosbaez

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