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 @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.
John Carlos Baez
DougMerritt (log😅 = 💧log😄)
ma𝕏pool
Jacques Carette
markusde
Philip Zucker
Andreas Christophilopoulos