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