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