I don't want to formalize any of my work on mathematics.

[martinescardo@mathstodon.xyz]

@hallasurvivor

It is not clear who specifically you are replying to. I hope it is not me.

@johncarlosbaez @andrejbauer @dougmerritt @JacquesC2 @pigworker @xenaproject

[dlakelan@mastodon.sdf.org]

@johncarlosbaez
So, while I think of formalism as a needed tool, I'm also with John in thinking that formalism is not always helpful. if formalism was enough we could replace all math books by the axioms of ZFC and be done with it... everything else left as an exercise for the reader
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject

[hallasurvivor@sunny.garden]

@MartinEscardo

Sorry, let me adopt your convention to make my reply more clear -- but you can tell I was replying to John since it's his post that show up above mine when you click my post (at least on my instance)

@johncarlosbaez @andrejbauer @dougmerritt @JacquesC2 @pigworker @xenaproject

[martinescardo@mathstodon.xyz]

@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

[cbaberle@mathstodon.xyz]

Having spent several years in the trenches of formalized mathematics by now, I'm actually more sympathetic @johncarlosbaez 's line of thinking than I used to be, but I think there's nothing about formalized mathematics *per se* that forces this to be the case.

The way I've come to use proof assistants/etc. over the years actually, counterintuitively, ends up making math more "empirical," in a way. My informal proofs and ideas become "hypotheses" I can "test" by attempting to find a formalism and suitable abstractions that make them checkable by a computer. And like any good scientific experiment, this quickly becomes an iterative process—take some informal ideas, attempt to formalize them, get some data back about what ends up being difficult, refine the ideas, repeat until a satisfactory equilibrium is found. And this process itself can lead to a lot of "a ha" moments and "radical" new ideas, itself.

As already noted, however, this process carries the risk of railroading one's thoughts into those ways of thinking that are more easily formalized in a particular system. But imo this is a failure of that particular system to be sufficiently syntactically/semantically flexible, and not of formalism/interactive theorem proving in general.

The future I hope for, and which I am actively building toward, is one in which we have general systems for defining, simulating, and verifiably translating between different logical/formal systems, so that if someone has a new mathematical idea they want to try out it's easy to get up and running with a system for testing it and relating it to other frameworks.

@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject

[mevenlennonbertrand@lipn.info]

@MartinEscardo Re: trusting C code, I heard horror stories about compilers for aeronautics, where one of the criteria for acceptance is that the "compiler" is very transparent and that the assembly code is auditable on its own. Apparently, getting these sort of people to accept an optimising compiler, even CompCert, was a hard battle… (But it was won!)

[johncarlosbaez@mathstodon.xyz]

@yakmacker - That would be cool. I will let someone else work on this, while I spend my limited remaining years thinking about the mysteries of math and physics that intrigue me.

[johncarlosbaez@mathstodon.xyz]

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

[jacquesc2@types.pl]

@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

[mc@mathstodon.xyz]

@JacquesC2 @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject I feel like there is a bit of a selection bias here. Would you say that formalization is as useful as a blackboard for eg number theory or geometric measure theory, as it is for type-theory/logic/computer science?
There is a huge UX problem, due to the fact that most mathematical research is done with objects and methods that fit badly in the current text-based, heavily formal (I don't know how to say this better) proof assistants. So my impression is that for most mathematics working formalization-first would be as painful and counterproductive as it would be for a PL/type theorist to work only on a whiteboard.
Hopefully this will change in the future! I do believe that formalization is very useful for mathematics.

[ohad@mathstodon.xyz]

@mc These areas might be more painful, but they contain mistakes. I found a few measure theoretic mistakes in some recent papers / theses over the last year or two.

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

[andrejbauer@mathstodon.xyz]

@johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject Well, it should be obvious, but let me say it anyway.

We need mathematicians of every kind: the thinkers, the dreamers, the formalizers, and even physicists.

[andrejbauer@mathstodon.xyz]

@mc @JacquesC2 @cbaberle @johncarlosbaez @dougmerritt @MartinEscardo @pigworker @xenaproject I'd go further and "blame" the philosophers of language, too.

[boydstephensmithjr@hachyderm.io]

@johncarlosbaez @MartinEscardo It took me weeks to finish my first non-trivial proof (preservation in an STLC). I'd think there's stuff that can be knocked out in a few hours that still retain the flavor, but no example leaps to mind.

[jacquesc2@types.pl]

@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@mathstodon.xyz]

@mc I definitely agree with this, and I have a bunch of thoughts about fixing it. Some programmatic remarks:

- Interactive theorem proving and text-based representations are already uneasy bedfellows. Let's embrace the "interactive" part and move to true structure editing where proof data is stored as abstract syntax trees and the language provides an open protocol for interfacing with such ASTs, on top of which one can implement whatever UI one pleases. Text-based editing becomes just one such "view" of the underlying proof data.
- A lot of "ordinary" math comes down to: draw a structured graph (in *both* senses of the word "graph") of some sort, and make some conclusion based on its structure. By now there's plenty of existing work on compiling things like commutative diagrams/string diagrams/etc. to syntax trees, etc., and we can and *should* make use of this work to provide more convenient interfaces to ITPs, via protocols as above.
- Interactive theorem proving deserves interactive documentation. We should have an analogue of Jupyter/Mathematica Notebooks for ITPs where different editor UIs can be mixed and matched, data can be displayed in a variety of formats, etc.

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

[johncarlosbaez@mathstodon.xyz]

@hallasurvivor - I don't think Grothendieck broke out of existing formalisms in quite the way I'm talking about. Though it broke radically new ground, all his work was rigorized very quickly. The people I mentioned did work that either took a century or more to make rigorous, or is still in process of being brought into the fold of rigorous mathematics. I'm talking about Newton's calculus, Euler's manipulations of divergent series to compute the zeta function, Feynman's path integrals, and the many path integral "proofs" given by Witten.

There are dozens of less famous but still interesting examples. I would never have written a paper about the Cobordism Hypothesis (and the still less finished Tangle Hypothesis and Generalized Tangle Hypothesis) if I had been thinking about formal definitions or proofs.

(That's an example that comes from outside analysis! But my other examples suggest analysis is a lot more future-leaning than algebra, in the sense of racking up debts against future formalization.)

[johncarlosbaez@mathstodon.xyz]

@andrejbauer - I agree: I want a diversity of approaches. Quotes like "It forces you to think about mathematics in the right way" are what scare me - together with the money that's getting poured into Lean right now, which could fool a young mathematician into thinking this is "the" right way to do math.

I have no fear that *you* will be pressured into doing anything you don't want to, just because it's the hot new trend.

[robjlow@mathstodon.xyz]

@dpiponi @johncarlosbaez I managed to get as far as a DPhil without any formal (sorry) education in the foundations of maths. The only times I recall it rearing its head were the passing comments in topology that Tychonoff's theorem needed the axiom of choice, and likewise in measure theory for non-measurable sets.

[sjb@mstdn.io]

@johncarlosbaez @andrejbauer You don't have to think in the formally correct way, but it helps to know what the formally correct way is.