hckrnws

This reminds me of a fun experience I had in grad school. I was working on writing some fast code to compute something I can no longer explain, to help my advisor in his computational approach to the Birch and Swinnerton-Dyer conjecture. I gave a talk at a number theory seminar a few towns over, and was asked if I was doing this in hopes of reinforcing the evidence behind the conjecture. I said with a grin, "well, no, I'd much rather find a counterexample." The crowd went wild; I've never made a group of experts so angry as that day.

Well, I never was much of a number theorist. I never did come to understand the basic definitions behind the BSD conjecture. Number theory is so old, so deep, that writing a PhD on the topic is the step one takes to become a novice. Where I say that I didn't understand the definitions, I certainly knew them and understood the notation. But there's a depth of intuition that I never arrived at. So the uproar of experts, angry that I had the audacity to hope for a counterexample, left me more curious than shaken: what do they see, that they cannot yet put words to?

I am delighted by these advances in formalism. It makes the field feel infinitely more approachable, as I was a programmer long before I called myself a mathematician, and programming is still my "native tongue." To the engineers despairing at this story, take it from me: this article shows that our anxiety at the perceived lack of formalism is justified, but we must remember that anxiety is a feeling -- and the proper response to that feeling is curiosity, not avoidance.

> The crowd went wild; I've never made a group of experts so angry as...

Also not a number theorist...but I'd bet those so-called experts had invested far, far too many of their man-years in that unproven conjecture. All of which effort and edifice would collapse into the dumpster if some snot-nosed little upstart like you, using crude computation, achieved overnight fame by finding a counter-example.

(If I could give my many-decades-ago younger self some advice for math grad school, one bit of that would be: For any non-trivial "Prove X" assignment, start by spending at least 1/4 of my time budget looking for counter-examples. For academic assignments, that's 99% likely to fail. But the insight you'll get into the problem by trying will be more worth it. And the other 1% of the time you'll look like a genius. And - as soon as you attempt real math research, those odds shift enormously, in favor of the counterexample-first approach.)

> All of which effort and edifice would collapse into the dumpster if some snot-nosed little upstart like you, using crude computation, achieved overnight fame by finding a counter-example.

Not at all. In fact, if I had found a counterexample, it would cause a flurry of new research to quantify exactly how wrong the BSD conjecture is. Such a finding would actually be a boon to their career! That's why my response is curiosity, and not to sneer at them for protecting their extremely secure tenured careers.

Edit 1: And if you think you've found a counterexample to a long-standing conjecture with a computation, you'd better be damned sure that your computation is correct before opening your mouth in public. And that takes a ton of work in the case of the BSD conjecture, because you've almost certainly identified a bug in the extremely complex code underlying that computation. If I ever thought I was holding onto such a counterexample, I'd approach a human calculator like Ralph Greenberg as my first step (after internal checks: re-running the code on another computer to rule out cosmic bit flips, and perhaps running more naive, unoptimized implementations).

Edit 2: This attitude pervades my software development career, and I've brought it to my foray into superconducting circuit design: a bug report brings joy to my life, and I aim to shower the reporter with praise (which may involve chocolate). There is nothing more satisfying than being proven wrong, because it helps us collectively move toward greater truths.

> Edit 2: This attitude pervades my software development career, and I've brought it to my foray into superconducting circuit design: a bug report brings joy to my life, and I aim to shower the reporter with praise (which may involve chocolate). There is nothing more satisfying than being proven wrong, because it helps us collectively move toward greater truths.

Not to mention that the usual wisdom of "don't kill the messenger" applies equally to bug reporters! Someone finding a bug in your code doesn't mean they willed it into existence; the bug would still be there even if you didn't know about it.

> my foray into superconducting circuit design

Curious, what do you work on? (I also research superconductivity.)

I've got a brief bio in my profile. The major thrust of my role is to develop architectures of digital/analog circuits for quantum computers, and I've lately been getting into device design. That's miles away from superconductivity research (at most, I could say I'm in applied superconductivity), so allow me to fawn a little... I'd love to be doing that kind of work!

Recently I found myself happy to find bug in code I have writtdn for those reasons.

To put a little color on the BSD conjecture, it states that the rank (0, 1, 2, 3, etc.) of rational points on an elliptic curve is related to the residue (coefficient of 1/q) of the L-function for the curve. There are some additional multiplicative factors, in particular the size of the Tate-Shafarevich group.

No one knows how to compute the size of that group in general (in fact no one has proved that it's finite!). Computing the rank of a curve via non-analytic means is more akin to a bespoke proof than a straightforward computation (see Noam Elkies' work).

So saying you're going to disprove BSD with blind computation is rather naive unless you're sitting on several career-defining proofs and not sharing them.

If the BSD rank conjecture were false, then the simplest counterexample might be an elliptic curve with algebraic rank 4 and analytic rank 2. This could be established for a specific curve by rigorously numerically computing the second derivative of the L-series at 1 to some number of digits and getting something nonzero (which is possible because elliptic curves are modular - see work of Dikchitser). This is a straightforward thing to do computations about and there are large tables of rank 4 curves. This is also exactly the problem I suggested to the OP in grad school. :-)

In number theory doing these sorts of “obvious computational investigations” is well worth doing and led to many of the papers I have written. I remember doing one in grad school and being shocked when we found a really interesting example in minutes, which led to a paper.

Then again it might just be a misunderstanding. And the so-called experts, in aggregate, turn out to be right more often than not.

Say I show up to a physics conference and proclaim that I hope my computational effort will disprove some major physical law. Well, you better have a good delivery, or the joke might not land well!

Sometimes people take things a little too literally after attending hours of very dry talks at serious seminars. I wouldn't read too much into it.

> All of which effort and edifice would collapse into the dumpster

Except it wouldn't, because the work towards the BSD would still be right and applicable to other problems. If someone proved the Riemann hypothesis false, all of our math (and there is a lot of it) surrounding the problem isn't immediately made worthless. The same is true for any mathematical conjecture.

I don't doubt the rest of your comment might have played a role, however.

> Also not a number theorist...but I'd bet those so-called experts had invested far, far too many of their man-years in that unproven conjecture. All of which effort and edifice would collapse into the dumpster if some snot-nosed little upstart like you, using crude computation, achieved overnight fame by finding a counter-example.

Are you maybe confusing math academia for psychology or social sciences? There is no replication crisis in math, no house of cards of self-proclaimed experts riding on bullshit. Mathematicians are _actually experts_ at a deep and extremely rigorous technical field -- many of them are even experts at computational approaches to problems! -- and when outsiders and upstarts resolve old conjectures, mathematicians generally react by celebrating them and showering them with fame, job offers and gushing articles in Quanta.

Maths may not have a replication crisis like some other areas, but when I go to maths events, it seems widely agreed there are far too many papers with incorrect theorems, it's just no-one cares about those papers, so it doesn't matter.

It turns out to be very, very common (as discussed in the linked article) that when someone really carefully reads old papers, the proofs turn out to be wrong. They are often fixable, but the point of the paper was to prove the result, not just state it. What tends to save these papers is that enough extra results have been built on top of them, and (usually), if there had been an issue, it would have showed up as an inconsistency in one of the later results.

The trunk is (probably) solid, but there are a lot of rotten leaves, and even the odd branch.

> no house of cards

As I understand TFA, from a formalist’s perspective, this is not necessarily the case. People were building on swathes of mathematics that seem proven and make intuitive sense, but needed formal buttressing.

> _actually experts_ at a deep and rigorous technical field

Seeing as the person you’re addressing was a mathematics graduate student, I’m sure they know this.

Yep. Here's an easy-looking one, that lasted just under 2 centuries (quoting Wikipedia) -

> In number theory, Euler's conjecture is a disproved conjecture related to Fermat's Last Theorem. It was proposed by Leonhard Euler in 1769. It states that for all integers n and k greater than 1, if the sum of n many kth powers of positive integers is itself a kth power, then n is greater than or equal to k...

> ...

> Euler's conjecture was disproven by L. J. Lander and T. R. Parkin in 1966 when, through a direct computer search on a CDC 6600, they found a counterexample for k = 5.[3] This was published in a paper comprising just two sentences.[3]

> [3] - Lander, L. J.; Parkin, T. R. (1966). "Counterexample to Euler's conjecture on sums of like powers". Bull. Amer. Math. Soc. ...

What exactly are you saying this is an example of?

It's certainly not something that people believed and built stuff on the basis of; it was never regarded as anything more than a conjecture and I would be a little surprised if even one paper was published that took the conjecture as a hypothesis, even explicitly (i.e., "We show that if Euler's conjecture is true then ...").

It's also not, so far as I know, a case where anyone reacted with defensiveness, horror, insecurity, etc., when a counterexample was found. They published a paper in a reputable journal. They don't seem to have had much trouble getting it published, if they discovered the counterexample in 1966 and the paper was published in a 1966 issue of said journal.

So if you're suggesting that this is a case where "people were building on swathes of mathematics that seem proven and make intuitive sense, but needed formal buttressing", I'd like to see some evidence. Same if you're suggesting that this is a case where "so-called experts had invested far, far too many of their man-years in that unproven conjecture" and there'd be a hostile reaction to a counterexample.

On the other hand, if you're not suggesting either of those things, I'm not sure what the connection to the rest of the discussion is.

> What exactly are you saying this is an example of?

A prominent conjecture in number theory, taken quite seriously for centuries, but which was quickly and rather easily disproven once computers became powerful enough.

No, it is not a exact analogy for Fermat, nor BSD, nor Riemann, nor ...

My initial point of interest was u/bootby's comment - why the heck would a room full of experts (presumably noteworthy math professors) become so angry at some grad student's comment? Then /usr/baruz's comment, about things which "seem proven and make intuitive sense, but needed formal buttressing". On occasion, "seemed" and "intuition" prove to be wrong, and Euler was a pretty-good example that.

they didn't become angry, they became excited.

and a famous conjecture is by definition something for which all the experts know that its truth is UNKNOWN (even in cases where most experts believe it's true).

> Seeing as the person you’re addressing was a mathematics graduate student, I’m sure they know this.

The OP (u/boothby) was not the person I was addressing (u/bell-cot).

Does this not imply that /u/bell-cot had been a graduate student in mathematics?

> If I could give my many-decades-ago younger self some advice for math grad school

It's HN bread-and-butter to insist that all experts are wrong, and it must be because BIG <random field> is just protecting the sweet sweet lower middle-class living of being a tenured professor or something.

The worst part of middle-class life in the US is its precariousness. A guaranteed lower middle-class living for life is a pearl indeed.

> The crowd went wild

I am curious what a group of number theorists "going wild" looks like.. were they throwing chairs or are we talking slightly raised eyebrows?

Surely there was angry muttering.

Multiple people raising objections at once, each at a reasonable volume to speak to a large seminar room, and other people speaking to their immediate neighbor. If there was angry muttering, I don't recall it. But yes, a crowd of mathematicians going wild is still pretty chill.

There was a story that Fred Richman got involved in a wrestling match as a result of a disagreement over a proof one time.

I never heard the full story ... everybody in the department at NMSU where he was at the time would just make comments to each other of the form "Remember the time ...?" with a response "Fred's a beast".

Perhaps a chair tipped over at most.

> [...]this article shows that our anxiety at the perceived lack of formalism is justified, but we must remember that anxiety is a feeling -- and the proper response to that feeling is curiosity, not avoidance.

Beautiful sentiment, also in other areas of life, thank you.

I remember when I was a student a friend of mine telling me this guy was giving a seminar and he'd just completed day one and everyone was really excited he was going to prove FLT. Of course, the guy in question was Andrew Wiles. He then spent months patching up problems they found prior to publication and finally the whole thing got published. It was a hugely exciting thing when you were studying mathematics.

All of which is a long way of saying the line "the old-fashioned 1990s proof" makes me feel _really_ old.

As a CS undergrad at Berkeley in the 90's I took an upper division math class in which we worked through the "old school" proof which was brand new and exciting then. Pretty much everyone else in the class was a math grad student. I don't think I understood more than 20% of the material! :)

I took that class with you! It was amazing. Here are my notes: https://wstein.org/books/ribet-stein/

And the professor who taught that course won a major prize today: Ribet to Receive 2025 AMS Steele Prize for Seminal Research - https://www.ams.org/news?news_id=7391&fbclid=IwZXh0bgNhZW0CM...

Thanks for sharing that! Very cool.

There was a great documentary TV shown about this story.

> Lean did that irritating thing which it sometimes does: it complained about the human presentation of an argument in the standard literature, and on closer inspection it turned out that the human argument left something to be desired.

Tongue-in-cheek irritation aside, this is actually awesome. I think Lean (and other theorem provers) are going to end up being important tools in math going forward.

Compilers have this very same habit!

Yes. In fact, Lean is a compiler and type checkers are theorem provers (by the Curry-Howard correspondence). Proofs are programs!

And Mathematics is Computer Science. Took me most of a lifetime to realize this.

I'd argue for the converse: Computer Science is Mathematics

> I'd argue for the converse: Computer Science is Mathematics

The space of programs is arguably larger than the space of mathematical systems, because programs can be logically inconsistent. This suggests that mathematics is a logically consistent subset of computer science, not the other way around.

And then you are wrong because everything now theorized into CS was already a thing in Math since long ago.

Lisp? Knuth and computation? Lambda Calculus did it before. ] https://en.m.wikipedia.org/wiki/Lambda_calculus

And, before computers, we had these:

https://en.m.wikipedia.org/wiki/State_machine

https://en.m.wikipedia.org/wiki/Control_theory

Let's just say there is a really big overlap between the two. And each one can learn from the point of view of the other.

Then we have the ghosts of information and category theories underpinning/influencing them all (including physics) (to some degree)

There are statements provably true about the natural numbers that can’t be proven in first order PA. Are such statements part of computer science? If so, how?

That question contains so many false or unnecessary assumptions that it would take far longer to unpack them than it took you to type them, so I will limit myself to the observation that we do not even remotely confine ourselves to first order anything in computer science, nor should we.

What false assumption did I make? I just pointed out a fact and asked a question. How many false assumptions could I have made with just one statement of fact and two questions? If you don’t have a valid answer to the question then don’t respond.

I’m a mathematician and not a computer scientist. The first order PA axioms are recursively enumerable. Hence it’s clearly something of interest to computer scientists. The second order PA axioms aren’t so…are they part of computer science? What do computer scientists think about proofs in second order PA? There are no computable models of ZFC so wouldn’t it be the case that while computer scientists deal with ZFC that ZFC isn’t part of computer science? what is your definition of computer science? Physicists deal with a vast amount of mathematics but math isn’t physics. In the same way mathematics isn’t computer science.

Overall I think most mathematicians would not consider mathematics as part of computer science.

To be fair I've heard gripes about statistics, and sometimes even probability being considered as part of mathematics.

The lines between (academic) fields are blurry -- academic fields do not form a set theoretic partitioning over areas of study.

The axioms of second order Peano arithmetic are certainly recursively enumerable, in fact you can pick a formulation that only uses a finite number of axioms. And second order arithmetic is much weaker than the type system of Lean, which is probably somewhere between Zermelo set theory and ZFC set theory in terms of proof-theoretic strength.

More generally, I think that computer scientists (in particular PL theorists and type theorists) are much more likely to use powerful logics than mathematicians, with the obvious exception of set theorists.

Do you have a reference for the second order induction schema being recursively enumerable? My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable. The second order Axioms are different than second order Arithmetic.

https://mathoverflow.net/questions/97077/z-2-versus-second-o...

In the following mathoverflow answer Nik says,

These are fundamental questions. We know that any computable set of axioms which holds of the natural numbers must also have nonstandard models.

The second order Peano Axioms are not computable since those axioms are categorical.

https://mathoverflow.net/questions/332247/defining-the-stand...

Are you of the opinion that mathematics is computer science? I have a hard time believing that the Jacobian Conjecture is computer science.

If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the second-order induction axiom (in your first mathoverflow link, this is called Z_2):

https://en.wikipedia.org/wiki/Second-order_arithmetic#The_fu...

An other equivalent option would be to use the language of second order logic, where you only need a finite amount of axioms, because the comprehension scheme is already included in the rules of second order logic. This one is PA_2.

Since these definitions do not refer to anything uncomputable such as mathematical truth, both systems are clearly recursively enumerable. This means that Gödel's incompleteness theorem applies to both, in the sense that you can define a sentence in the language of arithmetic that is unprovable in Z_2 or PA_2, and whose negation is also unprovable.

All of these considerations have little to do with models or categoricity, which are semantic notions. I think your confusion stems from the fact that model theorists have the habit of using a different kind of semantics for Z_2 (Henkin semantics) and PA_2 (full semantics). Henkin semantics are just first order semantics with two sorts, which means that Gödel's completeness theorem applies and there are nonstandard models. Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.

PS: I certainly do not consider mathematics to be included in computer science. Even though as a logician, I have been employed in both mathematics departments and computer science departments...

You know more than me on logic so I defer to your expertise.

https://math.stackexchange.com/questions/4753432/g%C3%B6dels...

Andreas Blass in the comments says that the Incompleteness results don’t apply to the second order Axioms (tabling about PA_2 here and not Z_2) and that the second order axioms are not computably enumerable. Maybe that’s the correct concept I was remembering from mathematical logic class. Don’t know if computably enumerable is the same as recursively enumerable but given what you’ve said I’m guessing they are different notions.

Consider the standard model of ZFC. Assume ZFC is consistent. Within this model there is one model of PA_2. Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.

Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.

If those axioms were recursively enumerable then the Incompleteness theorems would apply, right?

What Noah Schweber says here seems pertinent:

https://math.stackexchange.com/questions/4972693/is-second-o...

There's a bit of a definition issue at play here. When Andreas Blass and Noah Schweber say that there is no proof system for PA_2, they mean that there is no effective proof system that is complete for the full semantics. If you subscribe to their definition of a proof system, you end up saying that there is no such thing as a proof in PA_2, and thus that incompleteness is meaningless -- which I personally find a bit silly.

On the other hand, proof theorists and computer scientists are perfectly happy to use proof systems for second order logic which are not complete. In that case, there are many effective proof systems, and given that the axioms of PA_2 are recursively enumerable (they are in finite number!), Gödel's incompleteness will apply.

If you are still not convinced, I encourage you to decide on a formal definition of what you call PA_2, and what you call a proof in that system. If your proof system is effective, and your axioms are recursively enumerable, then the incompleteness theorem will apply.

Thanks for the reply.

> and that the second order axioms are not computably enumerable

He says that true sentences in second order logic aren't computably enumerable, he's not talking about the axioms.

> Don’t know if computably enumerable is the same as recursively enumerable

I've only ever seen them used as synonyms.

> Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.

What you call "Super PA" is called "the theory of PA". Its axioms are indeed not computably enumerable. That doesn't mean that the axioms of PA themselves aren't computably enumerable. And this much is true both for first and second order logic.

(edit: in fact, the set of Peano axioms isn't just computably enumerable, it's decidable - otherwise, it would be impossible to decide whether a proof is valid. This is at least true for FOL, but I do think it's also valid for SOL)

Thanks for the reply.

...it's decidable - otherwise, it would be impossible to decide whether a proof is valid.

Isn't that the whole issue with PA_2 vs. PA? In PA_2 with "full semantics" there is no effective procedure for determining if a statement is an axiom. In my mind this is what I mean by the incompleteness results not applying to PA_2. They do apply to Z_2 since that is an effective (computable?) system.

But Z2 is usually studied with first-order semantics, and in that context it is an effective theory of arithmetic subject to the incompleteness theorems. In particular, Z2 includes every axiom of PA, and it does include the second-order induction axiom, and it is still incomplete.

Therefore, the well-known categoricity proof must not rely solely on the second-order induction axiom. It also relies on a change to an entirely different semantics, apart from the choice of axioms. It is only in the context of these special "full" semantics that PA with the second-order induction axiom becomes categorical.

https://math.stackexchange.com/questions/617124/peano-arithm...

Thanks for the knoweledge. I'm going to read up more on this stuff.

> My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable

Incompleteness does apply to second order arithmetic (it applies to every logical system that contains first order PA), but due to different reasons: second order logic doesn't have a complete proof calculus. "Second-order PA is categorical" means that there is only one model of second-order PA, that is, for every sentence P, either PA2 |= P or PA2 |= not(P), but you'll still have sentences P such that neither PA2 |- P nor PA2 |- not(P) - and for "practical" purposes, the existence of proofs is what matters.

I think you are wrong in your first sentence. Take the collection of all true statements and make that your axiomatic system.

Andreas Blass in the comments says that Incompleteness does not apply to PA_2.

https://math.stackexchange.com/questions/4753432/g%C3%B6dels...

> Take the collection of all true statements and make that your axiomatic system.

A complete proof system needs to be able to derive Γ |- φ for every pair Γ, φ such that Γ |= φ. Not just when Γ is the complete theory of some structure. Completeness of first-order logic (and its failure for second-order logic) is about the logical system itself, while the incompleteness theorems are about specific theories - people often mix these up, but they talk about very different things.

> Andreas Blass in the comments says that Incompleteness does not apply to PA_2.

He says something rather different, namely that its "meaningless". That's a value judgement. Incomplete proof calculi for second order logic do exist (e.g. any first-order proof calculus) and for those, what I wrote is true. Andreas Blass would probably just think of this as an empty or obvious statement.

You know more than me. That is certain.

However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this. If I take the standard model of ZFC and collect all true statements in the one model of PA_2 and make that my axiomatic system then I have an axiomatic system that is not recursively enumerable and contains PA_1. It’s not a nice set of axioms. It’s not computable. But it shows that one can have an axiomatic system that contains PA_1 for which the Incompleteness theorems don’t apply.

Andreas wrote “meaningless” not “nonsensical”. I’m not a pedant but the former term evokes in me the idea of “does not apply in this situation becausethe hypotheses of the incompleteness theorem are not satisfied”.

From a mathematical logic book is the following. It’s the set up for the Incompleteness theorems.

Suppose that A is a collection of axioms in the language of number theory such that A is consistent and is simple enough so that we can decide whether or not a given formula is an element of A.

PA_2 is not such a system and as such the Incompleteness Theorems don’t apply. Maybe we are talking past each other. You know more than me.

> However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this.

That's a matter of semantics as to what you consider the first incompleteness theorem to be precisely (of which there are several variants). Gödel's proof itself doesn't directly work for second-order logic. But the statement "if Γ is some axiomatic system that satisfies certain conditions, then for any sound proof calculus there is a sentence that isn't provable from Γ in this calculus" is true in second order logic too, it's just that the "failure" happens much "earlier" (and is in some sense obvious) than in the case of FOL.

> PA_2 is not such a system and as such the Incompleteness Theorems don’t apply.

I'm really not all that familiar with second-order PA, but it is my understanding that the set of its axioms is decidable. It consists of a finite collection of axioms plus one schema (comprehension axiom) which is valid when it's instantiated by any given sentence - but deciding whether something is a valid sentence is easy. Therefore, what you quoted applies to second-order PA too.

From what you and the other person on this thread has said and from what I've read it appears that perhaps the following is true:

1. The axioms of PA_2 are recursively enumerable. 2. The full semantics of PA_2 are what cause categoricity.

It seems to me then that the crux of the matter is that the full semantics of PA_2 prevent there being an effective deductive system. I think Z_2 is constructed to get around the non effectiveness of the full semantics of PA_2 and is a weaker theory.

Anyway, thanks for the enlightenment.

With the caveat that I don't really understand second order logic well enough to say all that much about it, there's a debate in the philosophy of mathematics as to whether second-order logic should count as the foundational logic, since on the one hand most first-order theories aren't categorical (due to Löwenheim-Skolem) and on the other hand, second order logic (with full semantics) already presupposes set theory.

In any case, the reason why PA_2 is categorical is because the second-order axiom of induction allows quantification over arbitrary sets which allows you to say that "0 and adding the successor function to 0 arbitrarily often already gives you all natural numbers".

why should computer science be limited to things that are first order PA?

It shouldn’t and I didn’t say it should. I gave a fact and asked a question. Why is PA_2 computer science?

Computer science ought to be about computation, right? There are non-computable objects that mathematicians study. Is that part of computer science?

> There are non-computable objects that mathematicians study.

What's an example of such a non-computable object? Constructionism is based on the fact that every proof is a construction, which corresponds to a program, so you're claiming that there are proofs that do not correspond to any construction/program, and I'm curious what that might look like.

> Constructionism is based on the fact that every proof is a construction, which corresponds to a program

I don't think this is correct, even in constructive logic. Negative statements do not correspond to a construction, and in fact are the only statements in constructive logic that may be proven "by contradiction". But this means that every statement of non-constructive logic can be understood "constructively", if in a rather trivial sense, as a negative statement.

Linear logics may be a good way of exploring these issues in depth, since these allow for explicit "constructions" while preserving the sort of 'duality of negation' (i.e. flipping the direction of implications, or exchanging conjunctions w/ disjunctions) that's quite familiar within classical logic. Somewhat relatedly, there's also an interesting question of how much "construction" really is involved in typical constructive proofs, and whether that can be cleanly separated out from the more purely "logical" parts of the proof.

You're right that I'm being a little loose with terminology, as when I say "constructivism" I mean something more like "intuitionism", as with type theory.

Intuitionistic logic also allows for negative statements, which then are entirely non-constructive.

From a proofs-as-programs POV, this is just the observation that a proof is not just a program, but rather a program plus an explanation of why that program works correctly within its constraints, e.g. why it never ever tries to divide by zero. (This can be rephrased by saying that the program is both requesting and providing abstract "capabilities", i.e. information-free tokens, to its environment. Classical logic is then the logic of these capabilities, in the sense that providing a weak capability as output is essentially the same as asking for a strong capability from your environment as input.)

Constructivism is not mainstream mathematics.

The theorem that every vector space has a basis, something that is used fairly often, is actually equivalent to the axiom of choice, something that isn't valid in constructive logic. For many vector spaces you won't be able to write down a basis. And there are other examples, e.g. almost none of the automorphisms of C can be written down (only the identity and the conjugate map).

I'm aware that constructivism is not mainstream. What you've described are that such constructions are not available at this time (not comparable ones), but is there any evidence that comparable constructions are not possible even in principle?

Yes because the existence of a basis for arbitrary vector spaces is equivalent to the axiom of choice.

A derivation of the axiom of choice in Martin-Löf Type Theory, which is constructive:

https://plato.stanford.edu/entries/axiom-choice/choice-and-t...

This is exactly what I'm talking about, "every vector space has a basis" is not a provable statement in constructive mathematics because that ranges over non-constructive objects, but it can prove constructive equivalents like "every finite-dimensional or countable vector space has a basis".

I'm just not persuaded that this is not sufficient for any realizable mathematical construction. In my view, some non-constructive objects are non-realizable and so must ultimately serve only as convenient shortcuts that are ultimately eliminated when the math manifests in a real construction, either physical or computational. So if such things are merely artifacts of a particular formalism, then it should be possible to dispense with them entirely with a constructive or intuitionistic formalism.

That's why I'm looking for something that truly, fundamentally impossible for constructive mathematics, but that we know to exist, be true, valid, etc. that would contradict this position.

The set of statements about natural numbers that are true.

Using the law of the excluded middle is definitely a shortcut in such proofs, but there is no proof I'm aware of that shows no comparable constructive proof is possible. We reason with non-computable objects all of the time, such constructions are simply never fully materialized, and the need to materialize them are typically eliminated in later stages to prove concrete results. It's a good example but I don't think it's sufficient to exclude math from computer science.

>it would take far longer to unpack them than it took you to type them

Why is this a barometer for whether to answer a question or unpack assumptions?

Would it take too long or is it just that the margin is too small?

> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the experts” but not correctly documented. The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. For me, this is just one of many reasons why humans might want to consider getting mathematics written down properly, i.e. in a formal system, where the chances of error are orders of magnitude smaller. However most mathematicians are not formalists, and for those people I need to justify my work in a different way. For those mathematicians, I argue that teaching machines our arguments is a crucial step towards getting machines to do it themselves. Until then, we seemed to be doomed to fix up human errors manually.

It makes me think about how you get UI/UX/web designers who make (informal, imprecise) mockups and prototypes of their design ideas and interaction flows, they then hand these off to a developer to do the coding (formalise it, explain it precisely to the machine), and on the way the developer will inevitably find problems/holes in the designs (like an interaction scenario or code path not considered in the design, which could uncover a major design flaw), which the developer and/or the designer will have to patch somehow.

As in, design and development are different roles and require different mindsets, and most designers have a very strong resistance against working and thinking like a developer.

> consider getting mathematics written down properly, i.e. in a formal system

This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.

While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems, a huge amount of it obviously can, as is demonstrated by the fact that we can write it down in a reasonably rigorous way in a combination of conventional mathematical notation and plain English.

Nor is this in any way "a fundamental problem with using AI to do math".

There are two problems with this.

First, writing something down in English is very different from formalizing it. Natural language interacts with human brains in all kinds of complicated ways that we do not fully understand, so just because we can make a compelling-sounding argument in English doesn't mean that argument doesn't have holes somewhere.

Second, the incompleteness theorems apply only to given formal systems, not to formality in general. Given a system, you can produce a Godel sentence for that system. But any Godel sentence for a given system has a proof in some other more powerful system. This is trivially true because you can always add the Godel sentence for a system as an axiom.

This is a very common misconception about math even among mathematicians. Math produces only conditional truths, not absolute ones. All formal reasoning has to start with a set of axioms and deduction rules. Some sets of axioms and rules turn out to be more useful and interesting than others, but none of them are True in a Platonic sense, not even the Peano axioms. Natural numbers just happen to be a good model of certain physical phenomena (and less-good models of other physical phenomena). Irrational numbers and complex numbers and quaternions etc. etc. turn out to be good models of other physical phenomena, and other mathematical constructs turn out not to be good models of anything physical but rather just exhibit interesting and useful behavior in their own right (elliptic curves come to mind). None of these things are True. At best they are Useful or Interesting. But all of it is formalizable.

The other end of the Church-Turing intuition is that if we couldn't possibly do it then the machines can't do it either. What they're doing is the same, it's not only not magically less powerful it's also not not magically more powerful.

You seem to be imagining that Gödel is just a small problem you can carve off and ignore, but it applies for everything powerful enough to do arithmetic.

Of course we can have the AI muddle along with intuition, but that's not actually an improvement, our mathematicians can already use intuition and they've got a lot more experience.

It's a fundamental problem with using AI to do "intuitive" math, but not a fundamental problem with AI to do formal math.

As you have stared, a lot of mathematics can be formalized. For me the problem for AI with math is going to be the generative part. Validating a proof or trying to come up with a proof for a given statement may be within reach. Coming up with meaningful/interesting statements to proof is another completely different story.

Reading these threads makes me feel oddly familiar. This is the same discussion we have with Rust:

"You can't write everything in safe rust, therefore rust is worthless." vs "You must throw away all C code, or the whole industry will collapse"

except we have thousands of years of "unsafe" math, only a few decades of C.

> While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems

That's a misleading way of expressing that.

Math can be formalized as completely as we want, if we concede that some true statements will exist without a possible proof.

Hilbert's program assumed math to be completely decidable, i.e. that for every possible statement, a decision procedure could tell whether it was true or false. We know now that no such procedure can possibly exist. But merely writing down all known math in a formal system is completely doable. (Of course, formalization systems can be used to state any additional axioms that may be required of any given argument or development, so the original concerns about incompleteness are just not very relevant.)

TFA isn't about AI; it's about taking the same arguments mathematicians are already writing down semi-formally with a hand-wavy argument that it could be made completely formal, and instead/also writing them down formally.

In cases where the Hilbert machine applies, the mathematician writing down the semi-formal argument already has to state the new axioms, justify them, and reason about how they apply, and the proposal would just take that "reason about how they apply" step and write it in a computer-verifiable way.

> So this points to a fundamental problem with using AI to do math.

No it doesn't, AI like an LLM has no issues with stating two inconsistent propositions, just like humans, which is why both AI and humans can reason about all of mathematics, eg. Godel theorems is that a formal system cannot simultaneously be complete and consistent.

> This was already tried, and failed (Hilbert)

Who likely underestimated how hard it would be.

And who didn't have a 2024 computer on hand.

The reason Hilbert failed is because it’s mathematically impossible (Gödels incompleteness theorem).

> because it’s mathematically impossible

I guess the Lean devs can all pack and go home then. Also: how could they possibly miss Gödel's theorem, how careless of them.

Look, you’re taking my response out of context. I’m just stating that the reason Hilbert failed is not that he didn’t have a computer. Lean devs aren’t trying to do what Hilbert was.

If you're interested in this stuff at all, check out some code.

Example: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...

Also check out the blueprint, which describes the overall structure of the code:

https://imperialcollegelondon.github.io/FLT/blueprint/

I'm very much an outside observer, but it is super interesting to see what Lean code looks like and how people contribute to it. Great thing is that there's no need for unittests (or, in some sense, the final proof statement is the unittest) :P

Most (larger) Lean projects still have "unit tests". Those might be, e.g., trivial examples and counter examples to some definition, to make sure it isn't vacuous.

That's such a nice way to think about unit tests! (In this context and others.)

I think the better mapping of unit tests would actually be proofs of lemmas ?

I don't see why you would think that.

In such a project theorems and proofs are "the main point of the software". The unit tests make sure certain things don't go wrong by noticing when developers, e.g., mess up while refacing something. Also, people actually put the things I was talking about in a folder called "test"...

> The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be.

Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to "skip the details". What actually ends up happening is that if you want a rigorous proof that can be followed theoretically by every logical step, you actually need an expert to fill in a bunch of gaps that simply can't easily be found in the literature. It's only when such a person writes a book explaining everything that it might be possible, and sometimes not even then.

The truth is, a lot of modern math is on shaky ground when it comes to stuff written down.

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved.

Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer.

Here is an elementary example, which could be worked out by anyone with a good background in high school math. Prove the following statement: 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.

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

This flavor of statement comes up all the time in analytic number theory (my subject), would be regarded as obvious to any specialist, and in a paper would be invariably stated without proof.

To come up with a complete, rigorous proof would be long, and not interesting. No professional would want to read one.

I agree this attitude comes with some tradeoffs, but they do seem manageable.

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

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

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

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

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.

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.

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.

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.

"the proof is trivial"

"but can you prove it?

[10 minutes of intense staring and thinking]

"yes, it is trivial"

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

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

There'a a story that when someone wrote up a famous mathematician's work (Euler?), he found many errors, some quite serious. But all the theorems were true anyway.

Sounds like Tao's third stage, of informed intuition.

Back in Euler's time there as a lot of informality. The rigor of the second half of the 19th century was still some time in the future.

It's still incredibly painful as a learner though when things don't quite pan out. You start gaslighting yourself and then handwaved/convince yourself away that this must be true given how consistent all the "downstream" work is, and that you just don't fully understand it.

So, I agree with the author that this is super helpful, even if we know the proofs are "true" in the end

Studied math a long time ago and one of my profs was proud about not going into the details. He said "Once you did something 100 times, you can go and say -as easily observable- and move on."

I loved that some of the proof solutions in the back of mathematical logic book said, "Observe that ..." as the start of the proof. Our little study group definitely did not see how what followed was an observation we would have made.

Baker's little book of number theory made me work to get through every page...

I was an algebra major at the turn of the century and I hated that attitude.

For the prof, yeah, easily observable. What about the students who try to absorb that particular article? You already have to balance the main topic in your brain, and you get these extra distractions on top of it.

I have no background in math, so this might be naive, but shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps?

IIUC you're saying that basically someone with a mental database should be able to identify preconditions matching some theorem and postconditions aligned with the next statement from their mental database.

Or is there math that can't be expressed in a way for proof checkers to assess atm?

Edit: Or maybe proof checker use just isn't as wide-spread as I imagined. It sounds like the state statically typed languages in programming...

> shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps?

This is essentially exactly what Mathlib[1] is, which is Lean's database of mathematics, and which large portions of the FLT project will likely continually contribute into.

[1]: https://github.com/leanprover-community/mathlib4/

(Other theorem provers have similar libraries, e.g. Coq's is called math-comp: https://math-comp.github.io/ )

Has that ever blown up their faces?

I.e. a widely accepted proof that had a critical flaw due to hand waving?

If it hasn't, I would understand why they'd be cavalier about explicit details.

Yes, famously the Italian school of algebraic geometry ran into foundational issues. See https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge....

> it was absolutely clear to both me and Antoine that the proofs of the main results were of course going to be fixable, even if an intermediate lemma was false, because crystalline cohomology has been used so much since the 1970s that if there were a problem with it, it would have come to light a long time ago.

I've always wondered if this intuition was really true. Would it really be so impossible for a whole branch of mathematics to be developed based on a flawed proof and turn out to be simply false?

As mentioned by another comment, this is a big reason that Vladimir Voevodsky started his Homotopy Type Theory and Univalent Foundations program. He had see first hand a field collapse by a mistake in “first lemma on the first page” of a foundational paper. Arguably, he initial work on UniMath and the special year at IAS ending up in the HoTT book, pushed the whole formalization of mathematics topic forward to where it is today.

People hunt for counter examples to proofs they are working on. If the basis of their work is wrong, it's quite possible for one of the counter examples to also disprove the base theorem. So building on a faulty foundation is likely to reveal faults in the foundation.

Similarly, once in a while math gets applied and is used to make predictions. When the math is wrong, those predictions are wrong. And those wrong predictions draw a lot of attention.

I think it depends how widely used that branch of maths becomes. In fact, I'd say that the word "branch" is a bit misleading - for many theories it's much more of a "knot", with influences tying them to many many other theories across the mathematical landscape. And those theories are themselves tied to others, etcetera.

It would be a very strange situation if the foundation fell apart logically without any ramifications in the rest of this "knot". A huge swathe of free-floating mathematics that's completely internally consistent but for this one error? Difficult to imagine for me in the case of cohomology from the article.

I guess strictly speaking this is more of a philosophical stance - I like to believe that a lot of the current mathematics has been discovered "naturally" in some sense =)

This has happened before, see, e.g. the biography of Vladimir Voevodsky. Spoiler: the world kept spinning.

Russell’s paradox did the same thing. They had to go back to the drawing board.

For the past year or so, I've been trying (off and on) to formalise part of my undergraduate complex analysis course in Lean. It has been instructional and rewarding, but also sometimes frustrating. I only recently was able to fully define polar form as a bijection from C* to (-pi,pi] x R, but that's because I insisted on defining the complex numbers, (power) series, exp and sin "from scratch", even though they're of course already in mathlib.

Many of my troubles probably come from the fact that I only have a BSc in maths and that I'm not very familiar with Lean/mathlib and don't have anyone guiding me (although I did ask some questions in the very helpful Zulip community). Many results in mathlib are stated in rather abstract ways and it can be hard to figure out how they relate to certain standard undergraduate theorems - or whether those are in mathlib at all. This certainly makes sense for the research maths community, but it was definitely a stumbling block for me (and probably would be one if Lean were used more in teaching - but this is something that could be sorted out given more time).

In terms of proof automation, I believe we're not there yet. There are too many things that are absolutely harder to prove than they should be (although I'm sure that there's also a lot of tricks that I'm just not aware of). My biggest gripe concerns casts, in "regular" mathematics, the real numbers are a subset of the complex numbers and so things that are true for all complex numbers are automatically true for all reals[0], but in Lean they're different types with an injective map / cast operation and there is a lot of back-and-forth conversion that has to be done and muddies the essence of the proof, especially when you have "stacks" of casts, e.g. a natural number cast to a real cast to a complex number etc.

Of course, this is somewhat specific to the subject, I imagine that in other areas, e.g. algebra, dealing with explicit maps is much more natural.

[0] This is technically only true for sentences without existential quantifiers.

If this is your situation, you should absolutely be asking more questions on Zulip. It is really easy to get guidance on how to use mathlib, what things exist and where they are.

The issue with stacked casts is mostly solved by the `norm_cast` tactic. Again, ask more questions on Zulip - even if you don't ask about this in particular, if you suggest it in passing, or your code gives indications of an unnecessarily complicated proof style, you will get suggestions about tactics you may not be aware of.

One way you can focus a question like this if you don't know what techniques to use but just have a feeling that formalization is too hard, is to isolate an example where you really had to work hard to get a proof and your proof is unsatisfying to you, and challenge people to golf it down. These kind of questions are generally well received and everyone learns a lot from them.

I'm familiar with norm_cast and push_cast, but they don't always do what I expect them to do or solve all the problems. Then there's also the issue (in my experience at least) that in order to e.g. define the real exp or cos function you need to compose the complex function with the real projection and then manually use theorems such as "for all reals r, exp(r_inj_c(r)) = r_inj_c(re_exp(r))", which are easy enough to prove but it's still more work than in "regular" mathematics where you just say "re_exp = exp restricted to the reals" (and then implicitly use the fact that exp maps reals to reals).

I can usually find a way around such things but it does make proofs more tedious. As said, I'm sure I'm not using Lean optimally, but I wouldn't know what to ask for specifically, it's a case of "unknown unknowns".

> One way you can focus a question like this if you don't know what techniques to use but just have a feeling that formalization is too hard, is to isolate an example where you really had to work hard to get a proof and your proof is unsatisfying to you, and challenge people to golf it down.

Fair, that's something I could try. For example, my proof that cos 2 ≤ -1/3 (which is used for showing that cos has a zero in (0,2) with which I can define pi) is unreasonably complicated, while the proof on paper is just a couple of lines. There are a bunch of techniques used when estimating series, such as (re)grouping terms, that I found difficult to do rigorously.

This thread seems to be about good writing for math.

Okay, for some decades, I've read, written, taught, applied, and published, in total, quite a lot of math. Got a Ph.D. in applied math.

Yes, there are problems in writing math, that is, some math is poorly written.

But, some math is quite nicely written. (1) Of course, at least define every symbol before using it. (2) It helps to motivate some math before presenting it. (3) Sometimes intuitive statments can help.

For more, carefully reading some well-written math can help learning how to write math well:

Paul R.\ Halmos, {\it Finite-Dimensional Vector Spaces, Second Edition,\/} D.\ Van Nostrand Company, Inc., Princeton, New Jersey, 1958.\ \

R.\ Creighton Buck, {\it Advanced Calculus,\/} McGraw-Hill, New York, 1956.\ \

Tom M.\ Apostol, {\it Mathematical Analysis: Second Edition,\/} ISBN 0-201-00288-4, Addison-Wesley, Reading, Massachusetts, 1974.\ \

H.\ L.\ Royden, {\it Real Analysis: Second Edition,\/} Macmillan, New York, 1971.\ \

Walter Rudin, {\it Real and Complex Analysis,\/} ISBN 07-054232-5, McGraw-Hill, New York, 1966.\ \

Leo Breiman, {\it Probability,\/} ISBN 0-89871-296-3, SIAM, Philadelphia, 1992.\ \

Jacques Neveu, {\it Mathematical Foundations of the Calculus of Probability,\/} Holden-Day, San Francisco, 1965.\ \

This isn't just about good writing for math; the post author was trying to verify FLT as is developed in the literature, and along the way they discovered that a lemma underpinning a whole subfield is untrue, as was used. They nevertheless have confidence that the subfield is largely salvageable, by virtue of the faith that if it were bogus, someone would have already found negative results.

But now they had to find a suitable replacement to underpin the field.

Haha, that author is a funny writer. Very weird experience for that to be so readable, when I didn't understand probably half the content.

By the way, I found an excellent word for when a proof is disproven or found to be faulty, but that is esoteric enough that it has less risk of being misinterpreted to mean the conclusion is proven false: 'vitiated'. The conclusion might still be true, it just needs a new or repaired proof; the initial proof is 'vitiated'. I like how the word sounds, too.

Perhaps more delightful to the ears to hear that a proof has been disemboweled.

This article makes me very happy.

One of the many reasons I love math is the feeling I've always had that with it, we're building skyscraper-sized mental structures that are built on provably indestructible foundations.

With the advent of "modern" proofs, which involve large teams of Mathematicians who produce proof that are multiple hundreds of pages long and only understandable by a very, very tiny sliver of humanity (with the extreme case of Shinichi Mochizuki [1] where N=1), I honestly felt that math had lost its way.

Examples: graph coloring theorem, Fermat's last theorem, finite group classification theorem ... all of them with gigantic proofs, out of reach of most casual observers.

And lo and behold, someone found shaky stuff in a long proof, what a surprise.

But it looks like some Mathematicians feel the same way I do and have decided to do something about it by relying on the computers. Way to go guys !

[1] https://en.wikipedia.org/wiki/Shinichi_Mochizuki

This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha.

Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.

Don't think you should be intimidated just by reading the article itself. It is using several domain specific terms. But you would encounter that in many other contexts - for instance a group discussing an intricate board game you are seeing for the first time.

However, unlike board games where the concepts can be explained to you in a few minutes (usually it becomes clear only when you play), a lot mathematics especially algebraic geometry/number-theory can have many layers of dependencies which takes years to absorb.

It would be interesting to compare it to understanding a large open source project like the Linux kernel, well enough to contribute. I would say it is not so conceptually deep as mathematics of the article (while still having a few great ideas). But understanding the source would require familiarization with 'tedious details' which incidentally, what this article is also about.

So the issue, stated this way, is not so much raw talent as time and effort. This leads to the topic of motivation - finding something great in an idea can lead to investment in the subject. For those more talented, the journey might be easier.

Alan Kay's maxim is crucial - a change of perspective can simplify things relative to 80 extra IQ points. A long sequence of technical steps can be compressed into a single good intuitive definition/idea like the complexity of navigating a path becomes clear from a higher viewpoint.

Grothendieck, considered by many to be the best mathematician of the past century, made the point that there were several colleagues who were more proficient at symbolic manipulation. But, he was able to look at things with a more foundational perspective and could make great contributions.

Here's a good essay by Thurston "Proof and Progress in mathematics". https://arxiv.org/pdf/math/9404236

He discusses this problem of being intimidated by jargon.

Just a gentle reminder from somebody with a foot in each camp: computers were invented by mathematicians to accelerate computation. The field of Computer Science is a child of the field of Mathematics. Computer Engineering is its grandchild.

And yes, the desire for formalism has been stronger in the descendants than the ancestors for some time, but we're seeing that gap close in real time and it's truly exciting.

And, lets keep pushing the frontier of computation! We aren't just making better ad-delivery devices.

> about the same as the gap between us and everybody else

My bet: there is a very long list of skills for which the gap between you and a person randomly picked out the whole population is very large, and not in the direction you seem to think.

That’s true. It was poor phrasing on my part. But I do realize I’m really bad at a ton of things. I just meant in the math context.

[flagged]

"Please respond to the strongest plausible interpretation of what someone says, not a weaker one that's easier to criticize. Assume good faith."

https://news.ycombinator.com/newsguidelines.html

I just meant in the context of math skills, but I definitely acknowledge that it was poor phrasing on my part.

On the other hand get them to try and debug code. And then you might realize the redicilous amount of unwritten lore that software engineering has. OTOH software engineering has courses but you need to work with people to get good not just read books. Like math.

While true, there are some clues such as the correlation between someone's occupation and their IQ.

I don't even understand how you interpreted that to have anything to do with being "smarter or making more money". Get some more coffee dude.

Please don't respond to a bad comment by breaking the site guidelines yourself. That only makes things worse.

https://news.ycombinator.com/newsguidelines.html

Maybe less coffee :)

But how else would I power this machine that outputs theorems?

Erdős found stronger drugs

become comathematician and turn cotheorems into ffee

I am extremely disappointed at the replies from (some) experts. As a mathematician who has been worrying about the state of the literature for some time, I expected trouble like this---and expect considerably more, especially from the number theory literature between the 60s and the 90s. I also wonder how well 4-manifold theory is faring.

Much worse, this nonchalant attitude is being taught to PhD students and postdocs both explicitly and implicitly: if you are worried too much, maybe you are not smart enough to understand the arguments/your mathematical sense is not good enough to perceive the essence of the work. If you explain too much, your readers will think you think they are dumb; erase this page from your paper (actual referee feedback).

Also, like Loeffler in the comments, I don't trust the "people have been using crystalline cohomology forever without trouble" argument. The basics are correct, yes, as far as I can tell (because I verified them myself, bearing in mind of course that I am very fallible).

But precisely because of that, large swathes of the theory will be correct. Errors will be rare and circumstantial, and that is part of the problem! It makes them very easy to creep into a line of work and go unnoticed for a long time, especially if the expert community of the area is tiny---as is the case in most sub-areas of research math.

One of the best things about proof assistants is that they're not convinced by how "obvious" you think something is. It's much harder for a human to resist proof by social forces such as intimidation, confidence, and "it's well known".

Re: that dig at 4-manifolds

Are you aware of the book on [The Disc Embedding Theorem](https://academic.oup.com/book/43693) based on 12 lectures Freedman gave roughly a decade ago.

No, I am not an expert of 4-manifold theory and would not really understand most of the chapters. If this book fixes some of the literature issues in that field that is amazing! Does it finally resolve the issue of nobody understanding the construction of topological Casson handles?

Edit: I see from the MO comments "The fully topological version of the disc embedding theorem is beyond the scope of this book, since we will not discuss Quinn's proof of transversality."

This is the the talk by Dr de Frutos—Fernandez that Dr Buzzard mentions at the end: https://m.youtube.com/watch?v=QCRLwC5JQw0

Richard Feynman, while still a student at Princeton, found an error in some well known proof, and set himself a rule to double check every theorem he would use.

I don't remember the details of the story (I read surely your joking years ago), and remember being amazed by how much time that policy must have cost him.

But now I wonder that he didn't hit dozens or hundreds of errors over the years.

I'd be careful taking anything from "surely you're joking" as a fact btw.

There's a good popsci comms video on why here https://youtu.be/TwKpj2ISQAc?si=bpZOBy9WBGQzi6sk

She is more like complaining some (most?) RPF "bros" act like jerks, emotionally unstable, etc.

I guess the same can be said about many other "fanboi", and have little to do with the facts in the book

No, she's claiming that most of those stories were made up by a third guy with Daddy issues (if you want to be reductive)

You may want to watch this if Surely You're Joking read years ago is your main reference point: https://youtu.be/TwKpj2ISQAc

This makes me wonder if there'll ever be a significant bug discovered in Lean itself, breaking past formalisation work.

Lean has a small “kernel” that has been independently checked multiple times, and the rest of Lean depends on the kernel. A soundness bug is still possible, but pretty unlikely at this point.

https://lean-lang.org/lean4/doc/faq.html

Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.

That would be a bug in math itself, rather than a bug in Lean. It's possible, of course, but even less likely.

Fun fact, there have been 3 soundness bugs in lean 4 so far. (They were all fixed within hours.) I expect we have not yet found them all, but I also do not sleep poorly worried that mathematics will come tumbling down, because these are invariably implementation bugs (either in the literal sense of implementation of the system, or in the implementation of mathematics in the type theory). If something is wrong it is almost certainly going to be the system and not the mathematics. But I'm saying this as someone who works on the proof assistant itself (i.e. hold fixed the mathematics, vary the proof assistant). Kevin Buzzard will say the exact opposite because he is working on the mathematics (vary the mathematics, hold fixed the proof assistant), in which case the likely failure modes will be that a given proof is written poorly, a definition has incorrect behavior on edge cases, etc, but only the current proof is under threat, not some completely unrelated e.g. proof of infinitude of primes deep in the library.

For the problem to affect proofs, it would have to be in the type checker, and the type system isn’t really that complex. The good news is that every single user of Lean checks this works every day. Finding a flaw that literally everyone relies upon and doesn’t notice is pretty implausible.

Ahh, so maybe we should first focus on formalizing Lean itself?

Should I introduce you to https://arxiv.org/abs/2403.14064 ?

One of my favorite Horizon episodes is the FLT one that features Prof. Andrew Wiles' development of his proof (I have watched it many times). Of course, it is grounded in Fermat's margin note about his having a wonderful proof that couldn't fit in said margin. At the end of the documentary, the various mathematicians in it note that AW's proof certaintly wasn't what PdF had in mind because AW's proof is thorougly modern.

So I have wondered about PdF's possible thinking.

Now, the degenerate case of n=2 is just the Pythagorean Theorem

  c^2 = a^2 + b^2

Now, the PT is successful because the square b^2 can be "squished" over the corner of a^2, leaving a perfect square c^2. [Let's let the a^n part be the bigger of the two.]

  5^2 = 4^2 + 3^2

  25 = 16 + 9

  25 = 16 + (4 + 4 + 1)

Now, for cubes, we now know that a cube cannot be "squished" onto another cube's corner in such a way that makes a bigger cube.

I'm not up for breaking out my (diminishing) algebra right now (as it's a brain off day), but that b^3 cube would need to break down into three flat sides, three linear edges, and the corner.

This fits my physical intuition of the problem and seems to me to be a possible way that PdF might have visualized the cubic form. Now, I have zero mathematical intuition about such things (or necessary math skills either), but the physical nature of the problem, plus the fact that we now know that the cubic and beyond don't work, leads me to wonder if this is an interesting approach. It also makes me curious to know why it isn't, if that is indeed the case, (which I assume is probable).

As to the n=4 and beyond, I would just hand-wave them away and say something like, "Well, of course they are more fractally impossible", which by that I mean that a real mathematician would have to say exactly why the n=3 case failing means that the n>=4 case would also not work. (My guess here is that there just becomes less and less possibility of matching up higher-dimensional versions of a two-term addition.)

Anyway, just a thought I had some years ago. I even built a lego model of the bits of cube spreading out along the corner of the a^3 cube.

I would enjoy learning why I'm so utterly wrong about this, but I found it a fun mental exercise some years ago that's been swimming around in my brain.

Thanks in advance if there are any takers around here. :-)

[And, my favorite Horizon episode is 'Freak Wave'.]

I believe Wiles' proof requires the case of n=3 (Euler), and n=4 (Fermat) separately. That is, Wiles' proof starts with n=5 for nontrivial reasons.

So it is more likely that Fermat saw n=4, and thought the rest would be similar.

Formalization of maths seems like an overwhelmingly huge task. A bit like Cyc but harder. Is there some kind of chain reaction likely to happen once a critical mass of math has been formalized so that it becomes easier to do more?

If anything, it's a relatively straightforward way to do what amounts to publishable work in mathematics. Besides the obvious point of being able to claim "I've dotted all the i's and crossed all the t's", formalized proofs are often more elegant than the original they're based on because refactoring a proof to be simpler, more general etc. and checking that it still goes through is comparatively easy - and obviously, mathematicians are interested in that.

The refactoring idea is interesting because I can imagine "proof compression" creating a less readable proof too, similarly to how a code one liner can be harder to read.

It is also utterly unlike in that the formalization of math actually has real impact. Cyc has never had any impact and almost certainly never will.

Yes.

What is the simplest proof of FLT these days? I don’t think elementary proofs exist

Nice story, and I'm glad formalization work is proceeding. "Details left as an exercise to the reader" is the bane of true knowledge.

When this topic comes up I love sharing this talk by Sussman; because every time I watch it again!

https://www.infoq.com/presentations/Expression-of-Ideas/

Someone had to post this video of a song about Fermat - even if it’s in Dutch - legend: https://youtu.be/X2AVi6RCgN8?si=ZnN9lMb-XuirZ20_

I’m happy to see so much work going into fixing human errors in mathematics in a rigorous way.

https://www.techrxiv.org/users/717330/articles/702287-on-fer...

Next target: the Langlands program ?

[dead]

[flagged]

42 surely?

I can only count to 4.