CIRCLE WITH A DOT

@mc
As a rule of thumb, I'd say if a domain has had 5+ formalizations already, then yes, formal-first works. Two or less, likely not.

My 5 might be too low.

@ohad @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject

@mc

This issue of fit (which is indeed related to linguistics) is why CASes have a huge leg up on ITPs regarding UX. But they also have their fit problems, never mind their correctness problems.

Mathematica's UI coupled with a nice ITP would be nice. That would need a complete rewrite of both halves to be viable. But that would be a vast improvement.

Then we'd be in a good position, as a community, to actually figure out the "next generation" system.

@cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject

@cbaberle said "And this process itself can lead to a lot of "a ha" moments and "radical" new ideas, itself."

I have found the same thing. When I am working on things that are not directly about formalized mathematics, but with using a proof assistant as a blackboard (echoing Martin's wonderful phrasing), I feel that I am much freer to make wild conjectures, because I can disprove them equally quickly.

The numbers of "models" of quantum programming based on traced monoidal categories (that did not in fact work) is staggering. The failures were usually quite subtle. My co-author(s) and I had convinced ourselves via 'paper math' that they worked, for each and every one of them.

@johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject

@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker On a more personal note, I'm strongly enjoying that all this work on proof assistants is forcing many many more people to think about meta-mathematics (and I don't mean just logic here, but all aspects of 'mathematics' as a subject of study.) /end

@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker On the more optimistic side:

• there is a lot of structure to mathematics, which is currently not very well leveraged, i.e. Universal Algebra and its many generalizations. But people are working on that (myself included).
• regardless of what some say, there is a lot of 'computational mathematics', which is currently not well supported by any system, and essentially eschewed by Lean+Mathlib. That requires thinking differently. Again, people are working on that.
• in fact, there is quite a bit more to math in general -- see the Tetrapod approach for one.

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

@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I agree with @andrejbauer 's take, including his skepticism of my comments on Lean choking things off: we're talking (implicitly) about different time scales. I'm witnessing a current funnelling of resources, which will cause short-term pain. Indeed this is unlikely to remain 'forever'.

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