Hacker News Reader

Comment by lostmsu | Hacker News Reader

Math is the most formal science there is. Why don't serious math journals require programmatically checked proofs for all publications, and instead rely on what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts?

P.S. Reviews are still needed to check novelty etc.

View on HN

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

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

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.

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

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

This is great work.

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.

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

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

Getting a proof, even in one that is amenable to computer verification into a form where you can actually verify it is a monumental task, like it can easily take multiple experts multiple years.

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.

> I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods.

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.

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

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.

More often than not mathematicians look for proofs of things they (and others) are already convinced in being true (or even already know for a fact). The automatic proof checking is just for that - making sure the proof is correct.

This sounds like a very dangerous attitude, considering that making any tiny mistake will cause you to be able to prove any statement. Of all people mathematicians should understand that.

Empirically, proofs with bugs get ironed out into proofs with less bugs, and the results almost always end up standing. Why mathematical proof seems to be as good as it is at avoiding proving false statements is a matter of contention, but practically speaking it works. There's very little incentive to computer check proofs because, as a practical matter, mathematics is not plagued with false "theorems."

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.

> mathematics is not plagued with false "theorems."

But you don't know that.

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

The answer given there by Manuel Eberl is more or less what I was trying to get at (and he is far more knowledgeable about it than I am). Lots of mathematicians find that the existing level of rigor in the field is enough.

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.

This is largely because in modern mathematics, people ignore or won't build on proofs that are too complicated for them to follow, and rely heavily on trust and networking effects for the remaining proofs that are too useful to ignore. Plenty of results (including big results) are published in mathematical journals each year, which are "known" to be flawed or sketchy, but never have a formal rebuttal, and if you want to build on a proof that doesn't have much followup work, and are having trouble understanding its argument, you're expected to ask around and find out whether the proof is worth pursuing or not. Proof assistants would enable people to trust much more complex proofs from much more junior mathematicians, rather than essentially requiring the community to reprove the same results over and over until they're satisfied, and IMO this is holding back mathematics more than many mathematicians realize.

> 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 into a computer system.

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.

Right, but the ordinary methods of doing mathematics seem to be so good that the vast effort required to encode proofs well enough for a computer to check vastly dwarfs the benefit, at least for now.

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.

Because programmatically checked proofs don't work the way you think they do.

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

I understand that you might need a code review for the proof to look nice, but the point of a checked proof is that you don't need a separate code review for correctness. If it checks (sans internal checker issues) - it is correct.

You still need to check that the definitions are correct. If you define `x^n = 42`, then proving FLT for `n > 2` is really easy. And proof checkers cannot check that you get the definitions right.

Thanks for pointing that out. This is still magnitudes less things to manually check for correctness than an entire proof.

There are some huge (not insurmountable) obstacles to this happening. The biggest one, as I see it, is that so many mathematical objects need to be formalised into the system so that a theorem can even be stated, let alone its proof checked. Coming up with useful (and correct) formalisms of these objects, objects that mathematicians use constantly every day, are entire research projects of their own.

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.

Is it possible to even check such a proof programmatically? Do we have that kind of technology? Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper?

> Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper?

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.

There is a language called lean which is popular among mathematicians. Here is an article: https://www.quantamagazine.org/building-the-mathematical-lib...

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

My question was specifically referring to these huge 500 proofs that only a handful of people have even attempted to understand. What is the upper limit of what our current state-of-the-art proof assistants can handle?

The problem is not the limit of what proof checkers can handle - that probably goes beyond all known math. The problem is that long standing theories that 500 page proof is based on are not yet transcribed into formal language, so you'd need to do them first.

> Math is the most formal science there is.

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

> ...what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts?

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.

The slides that mahogany linked to [1] may give you some insight into this question. They're pretty interesting.

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

For the same reason Google does not formally prove the correctness of their code. It's technically feasible but impossibly complex to actually achieve.

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

There are multiple ways in which Google Mail while behaving incorrectly still be usable. But a theorem is not only useless if it is incorrect, it is dangerous.

(Meta but I don't think the parent comment deserved to be downvoted. Maybe it's arguably wrong but it prompted replies that increased my understanding of the practice of maths.)

Thanks for this remark.

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.

> Math is the most formal science there is.

Can you prove that?

Formality is technically the degree of mathiness applied to a domain, since formal logic and any other framework of formalization decomposes to mathematics.

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.

But if you only have maps and no territory, can you still be said to be doing cartography? :)

Reply on news.ycombinator.com