... Because that would take 2+ orders of magnitude more work, and nobody has the time/attention budget for it.

This is sort of like asking: why did you single person write this 10-page short story instead of making a Hollywood-style feature film?

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.

[1] https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...

[2] https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...

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.

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.

It is fun to fight the proof checker though! :)

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.

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.

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.

Adding to this problem the intersection of mathematicians who understand computer aided verification and who understand a particular piece of research mathematics is often empty, and even if there are a handful of people who could do the necessary work they're often busy doing more interesting stuff.

Finally I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods. I think its unlikely that this will happen for a long time, for the simple reason that to feed a proof into a computer requires someone to dissect the proof to its logical bare bones in the first place, and the person doing the dissection is likely to notice any errors before they get round to feeding the problem into the computer.

Right, because that's not how it works. Errors aren't discovered after the proof has been translated into machine language because that is the only step of the verification. As soon as the code is written, the proof is verified. Necessarily, then, any error discovery has to happen before that.

Because mathematics has more or less worked fine for decades without it, and most mathematicians aren't programmers and aren't interested in it. Proofs are for understanding, not for technical correctness (though obviously the latter is very important). A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe (and, crucially, that their peers also already believe) into a computer system.

That's not to say proof checkers aren't interesting in their own right, but there's lots of really quite good reasons why mathematics goes without them almost all of the time. Formal methods bring a lot to computing, where our programs fall apart constantly, but mathematical proofs almost always don't fall apart. And in computing, almost all programs don't have formal proofs of correctness! If any area needs them, it's in computing, not mathematics. You might as well ask why every compiler doesn't come with a proof of correctness: because it's already hard enough to build a compiler, let alone the monstrosity that would be a formal proof.

The added benefit to a computer-checked proof is usually small to nil, and it's a ton of work. Like, way more work than just writing the proof.

Computing, on the other hand, is plagued with broken programs, and formal methods are still a very specialized area, even though the potential benefits are much greater in computing than mathematics.

But you don't know that.

There certainly were precedents: https://mathoverflow.net/questions/291158/proofs-shown-to-be...

Obviously the people who like proof assistants disagree, and they may be right. It could be that modern theorems are just too complicated to be adequately evaluated by unassisted humans. But mathematicians have been getting along just fine without them for a long time, so "why aren't we requiring computer-checked proofs of everything" has a very straightforward answer: mathematicians writ large aren't convinced of the benefit yet.

I guess the question is which of "convincing a human" or "convincing a computer" is considered the higher bar.

In any case, uncovering "what you believe that isn't so" is pretty important.

There's obviously been a lot of work done on proof assistants and maybe it will become easy and natural to formulate most proofs in a way a computer can check, but it's not anywhere close to that yet. The book explicating the proof discussed in the article is already 500 pages long, translating that into something a computer could check just isn't at all feasible yet.

And even programatically checked proofs are still programs. And programs still need code review.

There are some excellent talks by Kevin Buzzard about this, and where he sees it going in the future from a mathematician’s perspective. We’re getting there but progress is slow, and a large part of why it’s slow is that modern mathematics is fantastically complicated.

The point of the checked proof is that your final theorem is almost definitely correct (you did not make mistakes in your deductions, unless the proof checker has a serious bug) if you can convince computer it derives from your axioms.

You can convince humans without your proof being correct thought, because they might not spot an error.

A more recent article as well: https://www.quantamagazine.org/lean-computer-program-confirm...

That's assuming you ascribe to viewing math as science.

> Why don't serious math journals require programmatically checked proofs for all publications

Presumably it has something to do with why formalized mathematics is rare: it's hard. Even relatively simple concepts become quite hard to deal with when fully formalized. I suspect that mathematics on this level is simply not amenable to the treatment that you envision (at least today).

I kinda feel like this question answers itself. On the other hand, I can't imagine this quagmire lasting another century, but the machine-assisted proof ecosystem hasn't reached adolescence yet.

[1] https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundatio...

Fully formalizing a proof with a tool like Coq or Isabelle is in and of itself a nontrivial problem.

It is amusing to see this behavior, considering the comment is a question, to which responses seem to favor answer "no".

The only part of the comment, that is actually a statement about peer review in mathematics being as bad or even worse in terms of assessing correctness, than reviewing large code changes. And nobody argues against that.

Can you prove that?

So... it's a tautology. Math is the most mathy math. Biology or psychology are less mathy maths.

https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

Having provablility holes in the formal system doesn't imply the existence of other systems that could be decomposed from currently known or unknown symbols. In this universe, information at the level of string theory seems to describe the limits, so math, as she is wrote, is as formal as it gets.

The map is not the territory, so math, as a map, will always be less "formal" than reality itself. It's pretty firmly in second place, though.