Hacker News Reader

> I don't think this is easily resolved.

It is technically resolvable. Just insist on Lean (or some other formal verifier) proofs for everything.

It looks to me like math is heading that way, but a lot of mathematicians will have to die before its the accepted practice.

Mathematicians who are already doing formal proofs are discovering it have the same properties as shared computer code. Those properties have have lead to most of the code executed on the planet being open source source, despite the fact you can't make money directly from it.

Code is easy to share, easy to collaborate on, and in the case of formal proofs easy to trust. It is tedious to write, but collaboration is so easy that publishing your 1/2 done work will often prompt others to do some of the tedious stuff. Code isn't self documenting unless it's very well written, but even horrible code is far better at documenting what it does than what you are describing.

> Just insist on Lean (or some other formal verifier) proofs for everything.

This is not an easy change at all. Some subfields of math rely on a huge amount of prereqs, that all have to be formalized before current research in that field can insist on formal proofs for everything as a matter of course. This is the problem that the Lean mathlib folks are trying to address, and it's a whole lot of work. The OP discusses a fraction of that work - namely, formalizing every prereq for modern proofs of FLT - that is expected to take several years on its own.

> Just insist on Lean (or some other formal verifier) proofs for everything

Lean is too inflexible for this, in my opinion. Maybe I'm not dreaming big enough, but I think there'll have to be one more big idea to make this possible; I think the typeclass inference systems we use these days are a severe bottleneck, for one, and I think it's very, very tedious to state some things in Lean (my go-to example is the finite-dimensionality of modular forms of level 1 - the contour integral is a bitch and has a lot of technicalities)

I agree, although I don't see a better solution: typeclass inference is trying to "quasi-solve" higher unification, which is unsolvable. The core tactics writers are already doing wizard-level stuff and there is more to come, but the challenge is immense.

By the way, if you are a meta-programming wizard and/or a Prolog wizard, please consider learning Lean 4 or another tactics based proof assistant. I think they will all welcome expert assistance in the development of better tactics and the improvement and debugging of current ones.

You might as well have written that mathematicians should stop doing mathematics. If every mathematician were to work full time on formalizing theorems in proof assistants, then no living mathematician would ever do original research again -- there is simply too much that would need to be translated to software. And to what end? It's not as if people suspect that the foundations of mathematics are on the verge of toppling.

> Code is easy to share, easy to collaborate on [...] collaboration is so easy that publishing your 1/2 done work will often prompt others to do some of the tedious stuff

Here's an experiment anyone can try at home: pick a random article from the mathematics arxiv [1]. Now rewrite the main theorem from that paper in Lean [2]. Did you find this task "easy"? Would you go out of your way to finish the "tedious" stuff?

> even horrible code is far better at documenting what it does than what you are describing

The "documentation" is provided by talking to other researchers in the field. If you don't understand some portion of a proof, you talk to someone about it. That is a far more efficient use of time than writing code for things that are (relatively) obviously true. (No shade on anyone who wants to write proofs in Lean, though.)

---

[1] https://arxiv.org/list/math/new

[2] https://lean-lang.org/theorem_proving_in_lean4/dependent_typ...

> but to truly provide all the details would make papers far, far longer.

I think what we need in math is that eventually, a collection of frequently cited and closely related papers should be rewritten into a much longer book format. Of course some people do that, but they hardly get much credit for it. It should be much more incentivated, and a core part of grant proposals.

Donald Knuth's literate computing could be an example to follow:

combine lean prove language with inline English human language that explains it. Then, Lean files can be fed into Lean to check the proof, and LaTeX files can be fed into LaTeX to produce the book that explains it all to us mere mortals.

This is already happening, by the way, and some Lean projects are being written in this way. Not only for the reader, but the proof writers themselves tend to need this to navigate their own code. Also check Lean 4 Blueprint, which is a component in this direction.

Isabelle proving environment implements this idea since at least 2005 when I started using it. One can interleave formal proofs and informal commentary in a theory file and one of the artifacts is a "proof document" that is a result of LaTeX processing of the file. Other options exist as well where the file is exported to HTML with hyperlinks to theorems and definitions referenced in a proof. There are also custom HTML renderers (since 2008) where a reader can expand parts of the structured proof when they want to see more details.

Agda 1 (more specifically, the included UI program known as Alfa) implemented an automated translation from formal proof to natural language, driven via Grammatical Framework. This requires writing snippets of code to translate every single part of the formal language to its natural language equivalents, at varying levels of verboseness - for example, (add a b) could become "a + b", "the addition of a and b", "adding b to a" and so on. Similar for proof steps such as "We proceed by induction on n", properties such as "is commutative" etc. The idea gets reimplemented every now and then, in a variety of systems. Of course the most compelling feature is being able to "expand out" proof steps to any desired level of detail.

> there exist constants C, X > 0 such that for every real number x > X, we have

>> log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx.

These problems are only "uninteresting" to the extent that they can be "proven" by automated computation. So the interesting part of the problem is to write some completely formalized equivalent to a CAS (computer algebra system - think Mathematica or Maple, although these are not at all free from errors or bugs!) that might be able to dispatch these questions easily. Formalization systems can already simplify expressions in rings or fields (i.e. do routine school-level algebra), and answering some of these questions about limits or asymptotics is roughly comparable.

The problems are uninteresting in the sense that the audience for these papers doesn't find them interesting.

In particular, I'm not making any sort of logical claim -- rather, I know many of the people who read and write these papers, and I have a pretty good idea of their taste in mathematical writing.

Well, you did claim that the problem could be worked out with simply high school math. It would certainly be 'interesting' if such problems could not be answered by automated means.

(For example, I think many mathematicians would find the IMO problems interesting, even though the statements are specifically chosen to be understandable to high-school students.) The problem of how to write an automated procedure that might answer problems similar to the one you stated, and what kinds of "hints" might then be needed to make the procedure work for any given instance of the problem, is also interesting for similar reasons.

The example you gave, however, is obvious to every graduate student in any field that touches analysis or asymptotics. That is not the real problem; the real problem is proof by assertion of proof: "Lemma 4.12 is derived by standard techniques as in [3]; so with that lemma in hand, the theorem follows by applying the arguments of Doctorberg [5] to the standard tower of Ermegerds."

Too many papers follow this pattern, especially for the more tedious parts. The two problems are that it makes the lives of students and postdocs torture, and that the experts tend to agree without sufficient scrutiny of the details (and the two problems are intrinsically connected: the surviving students are "trained" to accept those kinds of leaps and proliferate the practice).

Frustratingly, I am often being told that this pattern is necessary because otherwise papers will be enormous---like I am some kind of blithering idiot who doesn't know how easily papers can explode in length. Of course we cannot let papers explode in length, but there are ways to tame the length of papers without resorting to nonsense like the above. For example, the above snippet, abstracted from an actual paper, can be converted to a proof verifiable by postdocs in two short paragraphs with some effort (that I went through).

The real motive behind those objections is that authors would need to take significantly more time to write a proper paper, and even worse, we would need actual editors (gasp!) from journals to perform non-trivial work.

I strongly agree with you, in the sense that many papers provide far fewer details than they should, and reading them is considered something of a hazing ritual for students and postdocs. (I understand that this is more common in specialties other than my own.)

The blog post seems to be asserting a rather extreme point of view, in that even the example I gave is (arguably!) unacceptable to present without any proof. That's what I'm providing a counterpoint to.

> (I understand that this is more common in specialties other than my own.)

True, analytic number theory does have a much better standard of proof, if we disregard some legacy left from Bourgain's early work.

I think Kevin Buzzard et al are aiming for a future where big, complicated proofs not accompanied by code are considered suspicious.

I wonder if being able to drill all the way down on the proof will alleviate much of the torture you mention.

The two problems are that it makes the lives of students and postdocs torture, and that the experts tend to agree without sufficient scrutiny of the details (and the two problems are intrinsically connected: the surviving students are "trained" to accept those kinds of leaps and proliferate the practice).

I think this practice happens in many specialized fields. The thing with math is that the main problem is the publications become inaccessible. But when you have the same sort of thing in a field where the formulations assumptions that aren't formalizable but merely "plausible" (philosophy or economics, say), you have these assumptions introduced into the discussion invisibly.

Using vague terms like "obvious" or "standard techniques" is doubtless wrong, but I would not see any problem in a paper basing its conclusions on demonstrations from a source listed in the bibliography, except that in many cases those who read the paper are unable to obtain access to the works from the bibliography.

Even worse is when the bibliography contains abbreviated references, from which it is impossible to determine the title of the quoted book or research paper or the name of the publication in which it was included, and googling does not find any plausible match for those abbreviations.

In such cases it becomes impossible to verify the content of the paper that is read.

This is a wider problem in general and an odd bit of history: scientific papers pre-date the internet, and as such the reference system exists pre-computation. the DX-DOI system is a substantial improvement, but it's not the convention or expectation - and IMO also insufficient.

Realistically, all papers should just be including a list of hashes which can be resolved exactly back to the reference material, with the conventional citation backstopping that the hash and author intent and target all match.

But that runs directly into the problem of how the whole system is commercialized (although at least requiring publishers to hold proofs they have a particular byte-match for a paper on file would be a start).

Basically we have a system which is still formatted around the limitations of physical stacks of A4/Letter size paper, but a scientific corpus which really is too broad to only exist in that format.

The issue with hashing is that it's really tricky to do that with mixed media. Do you hash the text? The figures? What if it's a PDF scan of a different resolution? I think it's a cool idea—but you'd have to figure out how to handle other media, metadata, revisions, etc, etc.

DOIs fix that.

Not a (former) mathematicien (but as a former PhD student in theoretical physics still some affinity with math): I remember being shocked when, having derived a result using pen and lots of sheets of paper, my co-promotor told me to just write '<expression one> can be rewritten as <expression two>' and only briefly explaining how (nothing more then a line or two), as the magazine we were to publish (and did publish) the article would not want any of those calculations written out.

Is there really not a centralized corpus of that kind of fundamental result you guys can use? I would have assumed that was "theorem #44756" in a giant tome you all had in your bookshelf somewhere.

Nope. Many important results have names that are familiar to everyone in the subfield, so you might say "by So-and-So's Lemma, this module is finitely generated". Failing that, you could maybe cite a paper or a book where the result appears, like "We can then conclude using Corollary 14.7 from [31] that...", where [31] is in your bibliography.

I think the resolution is being much less strict on paper appendix size. And slightly shortening the main body of a paper. Let the main text communicate to the experts. Let the appendix fill things in for those looking to learn, and for the experts who are sceptical.

I don't think that is a great example since it only takes a moment to see the loose bounds C, X = 3, e.

It would be annoying to have to code that kind of statement every time, but it wouldn't add that much to the effort.

Formalizing is still enormously hard, but I don't think that this is the example to hang the argument on.

To prove that you divide both sides by x and take the limit for x -> inf, applying L'Hopital rule the limit is zero, so there is such a C, any number greater than zero. The existence of such X is just the definition of limit when x tends to inf.

Another way, just using a cas (like maxima) to compute such limit: (%i1) limit( (log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4*x + 3)))/x,x,inf); the result is zero.

I don't think that's a good example, since it's obviously provably true and the proof is also obvious (either use well-known lemmas like log(poly(x)) in O(x^a) or show that lim_x->inf lhs/x = 0 via L'Hôpital's rule, differentiation algorithms and well-known limits at infinity).

I think if you let C=3 it isn't that long. The first two terms are less than x for x>5, the last term is also less than x for all positive x, done. Those lemmas are pretty easy to figure out.

It's not that trivial if we really insist on all the details. Let's assume x > 0 throughout. We can take sqrt(x) < x as a freebie.

An important lemma we need is that if f(x) is continuous on [a,b] and f'(x) > 0 on (a,b), then f(a) < f(b). For this, we need to write out the mean value thoerem, which needs Rolle's theorem, which needs the extreme value theorem, which gets into the definition of the real numbers. As well as all the fun epsilon–delta arguments for the limit manipulations, of course.

x/exp(sqrt(4x+3)) < x thankfully follows trivially from exp(sqrt(4x+3)) > 1 = exp(0). Since sqrt(4x+3) > 0, we just need to show that exp(z) is increasing. For this, we can treat the exponential as the anti-logarithm (since that's how my high school textbook did it), then show that log(z) is increasing, which follows from log'(z) = 1/z > 0 and our lemma.

For log(x^2+1) < x, we'll want to use our lemma on f(z) = z - log(z^2+1) to show that f(x) > f(0) = 0. Here, f'(z) = 1 - 2x/(x^2+1), for which we need the chain rule and the power rule (or a specialized epsilon–delta argument). Since x^2+1 > 0, f'(z) > 0 is implied by (x^2+1) - 2x > 0, which luckily factors into the trivial (x-1)^2 > 0. So ultimately, we break the lemma up into (0,1) and (1,x) to avoid trouble with the stationary point.

The trouble with problems like these is the whole foundation that the obvious lemmas have to be built upon. "Just look at the graph, of course it's increasing" isn't a rigorous proof. Of course, if you want to do this seriously, then you go and build that foundation, and on top of that you probably define some helpful lemmas for the ladder of asymptotic growth rates. But all of the steps must be written out at some point or another.

log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx.

I don't get why this is true. If C is 1 and x is 2

log(x^2+1) sqrt(2) + x/exp(sqrt(4*2 + 3)) is not less than 2.

The statement wasn't that it's true in general - only that there existing constants C and X>0 for which it is true for all x>X.

>Here is an elementary example, which could be worked out by anyone with a good background in high school math

WTF

>i.e. the left-side is big-O of the right.

Oh.

I didn't learn big O at high school though.

Calc AB covers it, and BC certainly gives you enough for a proof.

"the proof is trivial"

"but can you prove it?

[10 minutes of intense staring and thinking]

"yes, it is trivial"