Would it though? Are proof checkers much more complicated than LaTeX?
If mathematicians are in certain ways similar to developers, I'd expect them to hate fighting with the layout of their papers, and love fighting with a proof checker for the formulas.
Maybe half (?) of the basic undergraduate math curriculum has been formally verified, after decades of effort by large numbers of researchers. The proof under discussion here is significantly more complicated than anything that has ever been formally verified, as far as I understand. Disclaimer: I don’t know much about formal verification of mathematics, only what I have read from time to time on the internet.
It's not out of the question for research-level math to be formalized in proof assistants. Most notably, a landmark paper by Peter Scholze (a Fields medalist) was, at his request, formalized in Lean. Or at least, the important part was formalized in about 6 months. See [1] for the post where Scholze asks for help in formalizing the proof and explains why he thinks it's important - in this case it was a very gnarly proof of a theorem that could hopefully be used as a black box by other mathematicians. See [2] for Scholze's thoughts after the project succeeded, 6 months later.
But to be clear: a community effort by 20+ people, after 6 months of work, managed to make progress toward proving a theorem, including proving some of the trickiest technical parts. As I said before, this is like 2 orders of magnitude more effort than the original plain-language (slightly sloppy/underspecified) proof.
Scholze:
> I cannot read the proofs at all — they are analogous to referring to theorems only via their LaTeX labels, together with a specification of the variables to which it gets applied; plus the names of some random proof finding routines.
As someone whose research currently consists of proving things in proof checkers, I can confirm they are more complicated than LaTeX.
At one point, I had to prove n / 15 + n / 4 + (2 * n / 3 + 1) <= n, for positive n. Seems simple right? But first you have to multiply by 60 so that you're working over actual naturals. But then you have to contend with the fact that n / 15 * 15 <= n itself needs proof (they're not just equal, since n / 15 actually represents the floor or that quotient). Automatic tactics that simplify things for you help some, but it still ends up being a good 8 lines of code for such a trivial statement. When things like this can be handled fully automatically, then it will be ready for mainstream use.
> Are proof checkers much more complicated than LaTeX?
In terms of lines of code, no. In terms of the learning curve, yes -- latex does a very good job of getting out of the way and letting a mathematician just write in English, where proof assistants require rigid structure that doesn't remotely resemble how (most) mathematicians think.
In terms of runtime, oh my god, get out of town.
> In terms of runtime, oh my god, get out of town.
I think you're mixing two different things here. Runtime is large for proof assistants, e.g. programs that can actually generate pieces of proof for you. Specifically the generation part. Verification of a complete proof were all the steps are provided like you would do in a paper should not, AFAIU, take a long time.
The problem is that the way people write proofs, you don't go axiom by axiom. You might evaluate an integral in one step, or make an argument that some sequence is obviously asymptotically less than a function. Pretty much every step in a human proof requires a computer proof generation step to verify.
There might be a chicken and an egg problem. If knowledge of theoretical mathematics would be designed like a framework with good documentation what you mention would be solved by simply referring to the corresponding part of the framework.
But to get that more people would need to be involved into transcribing proofs into formal language. Ideally, everyone. This is a higher standard, and somebody needs to ask for it.
Fair point. I'm coming from the perspective that mathematicians don't like to fill in pesky details that experts in their respective fields can figure out in an hour or ten.
If mathematicians are in certain ways similar to developers, I'd expect them to hate fighting with the layout of their papers, and love fighting with a proof checker for the formulas.