[jimwhite42]

> It seems like it should be possible, in theory, but it takes too much work.

The definition of a valid mathematical proof that I've heard mathematicians use is if it convinces other mathematicians. I think there's integrity in depth in mathematical proofs for lots of reasons, tying back to an axiomatic basis is a lot of extra work for likely no benefit.

On formal mathematics, almost no mathematicians pay attention to this afaik. It's something that lives in philosophy departments, not mathematics.

[JonChesterfield]

> On formal mathematics, almost no mathematicians pay attention to this afaik. It's something that lives in philosophy departments, not mathematics.

In the old days there were philosophers. They sought truth through thought and wisdom. Some started to measure reality and compare thought against that measurement, but real philosophers paid little heed for it didn't matter.

Testing their theory became known as physics. It turned out the testing against reality can be used without the theory, which we call engineering. We still have philosophers and they still pay little heed to measurement.

There is a similar disaster inbound for mathematicians. Formal mathematics is tedious and mostly only shows things that you were pretty sure were true anyway, so why bother.

It turns out the physicists and engineers have unsportingly built machines which are really, really good at the tedious bookwork required by formal mathematics. That is going to go exactly the same way that introducing measurement to philosophy went for the philosophers.

[aleph_minus_one]

> There is a similar disaster inbound for mathematicians. Formal mathematics is tedious and mostly only shows things that you were pretty sure were true anyway, so why bother.

> It turns out the physicists and engineers have unsportingly built machines which are really, really good at the tedious bookwork required by formal mathematics. That is going to go exactly the same way that introducing measurement to philosophy went for the philosophers.

Formalized mathematics is just a very small subset of what mathematicians work on: in my observation people who work on (computer) formalized proofs often rather sit in CS departments.

[disconcision]

this may be changing. as we speak. terence tao has recently been working to formalize existing work in lean. and has already found a bug in one of his published proofs. i think there will always ish be a need for mathematical proofs in the contemporary sense, but at this point i don't think its too implausible to suggest a future where the mathematical mainstream moves towards some hybrid mathematical exposition of computationally verified artefact.

https://mathstodon.xyz/@tao/111287749336059662

[jimwhite42]

I think it's likely that axiomatic approaches, and formal approaches will continue to produce interesting results and have some effect on regular mathematics.

But this is very different to suggesting that most regular mathematics will switch to using formal proofs. There's a big ergonomics gap at the moment.

An analogy could be to look how pure mathematicians look down on applied mathematicians' work, the applied mathematicians don't care, they just get on with their own standards. You need regular mathematicians to choose to switch over en masse, what will compel them to do that?

[zmgsabst]

…success by Tao and Scholze in formalizing their work and gaining appreciable benefits such as correcting technical errors.

Which is happening right now — and the younger mathematicians who are supporting those efforts (and more broadly, things like Lean libraries) are gaining the experience while making the ergonomic changes.

That is, the person you’re replying to isn’t unaware of the historic problems: they’re pointing out that migration is starting now with early adopters like Tao and Scholze.

[jimwhite42]

I think a little hesitance on the overall success of these sorts of projects is prudent, given the history of axiomatic and formal expections and reality.

But let's say they make huge amounts of progress - they might improve the ergonomics enough that the formal foundations of mathematics will be brought into mathematics departments as a standard, legitimate and popular subject. But I still can't see how this would affect most mathematics.

[BoiledCabbage]

> But I still can't see how this would affect most mathematics.

It won't, in the same way that introducing physics didn't affect philosophers. They were still free to do philosophy. But most new innovation and innovators came up doing physics instead - and that's been where all the growth had been for centuries.

In the end ungrounded theory is better than nothing. But grounded theory beats out ungrounded theory hands down.

[mikhailfranco]

The canonical paper on this was written by De Millo, et al., but it has a rather ungrammatical and incomprehensible title that does it no favors. However, the al. include Lipton and Perlis, so listen up...

Social Processes and Proofs of Theorems and Programs

https://dl.acm.org/doi/pdf/10.1145/359104.359106 [pdf]

[bvssvni]

I think the most exciting work in mathematics today is in the formal foundations. However, I can also understand mathematicians who are thinking like this:

1. I only need normal congruence

2. I only need perfect information games

Under problems that are solvable using these two assumptions, there is little benefit in tying proofs back to an axiomatic basis. Once you drop one of these two assumptions, proofs get much harder and a solid foundation gets more important.