Fermat's Last Theorem – how it’s going

https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/

by verbify • 2 years ago

443 208 2 years ago

xenaproject.wordpress.com

munchler4• 2 years ago

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.

FredPret• 2 years ago

Compilers have this very same habit!

munchler4• 2 years ago

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

pennomi• 2 years ago

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

seanwilson• 2 years ago

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.

coliveira• 2 years ago

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.

hansvm• 2 years ago

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.

ur-whale4• 2 years ago

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.

lambdaone• 2 years ago

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

zozbot2348• 2 years ago

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

naasking9• 2 years ago

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.

bee_rider3• 2 years ago

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.

Etheryte• 2 years ago

[flagged]

analog31• 2 years ago

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

bee_rider3• 2 years ago

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

TechDebtDevin• 2 years ago

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.

dang2• 2 years ago

"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

ur-whale4• 2 years ago

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.

bee_rider3• 2 years ago

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.

boothby5• 2 years ago

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.

enugu• 2 years ago

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.

lincolnq• 2 years ago

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

staunton3• 2 years ago

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.

schoen• 2 years ago

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

pierrefermat1• 2 years ago

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

ur-whale4• 2 years ago

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

Retr0id• 2 years ago

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

pkoird2• 2 years ago

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

digama03• 2 years ago

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

moomin4• 2 years ago

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.

munchler4• 2 years ago

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

norlygfyd• 2 years ago

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.

digama03• 2 years ago

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.

vouaobrasil2• 2 years ago

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.

uffjedn• 2 years ago

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

brobdingnagians• 2 years ago

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.

inglor_cz• 2 years ago

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.

hyperthesis• 2 years ago

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.

pfdietz• 2 years ago

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.

hughesjj6• 2 years ago

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

impendia3• 2 years ago

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.

vouaobrasil2• 2 years ago

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.

ykonstant6• 2 years ago

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.

zozbot2348• 2 years ago

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.

brap• 2 years ago

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.

rstuart4133• 2 years ago

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.

devit• 2 years ago

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

bandrami• 2 years ago

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.

rocqua2• 2 years ago

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.

saberience• 2 years ago

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.

imprime• 2 years ago

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.

wbl2• 2 years ago

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.

ted_dunning3• 2 years ago

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.

rendaw• 2 years ago

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

JulianWasTaken• 2 years ago

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

paulddraper2• 2 years ago

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.

mydogcanpurr• 2 years ago

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

boothby5• 2 years ago

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.

bell-cot3• 2 years ago

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

isotypic• 2 years ago

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.

tux3• 2 years ago

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.

mostly_a_lurker2• 2 years ago

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.

brendanyounger• 2 years ago

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.

boothby5• 2 years ago

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.

awanderingmind• 2 years ago

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

mrintegrity• 2 years ago

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?

naasking9• 2 years ago

Surely there was angry muttering.

graycat• 2 years ago

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

jhanschoo• 2 years ago

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.

ykonstant6• 2 years ago

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.

cobbal• 2 years ago

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

zyklu5• 2 years ago

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.

ykonstant6• 2 years 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."

modeless• 2 years ago

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?

staunton3• 2 years ago

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

moomin4• 2 years ago

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

bubblyworld• 2 years ago

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

rocqua2• 2 years ago

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.

Atiscant• 2 years ago

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.

moomin4• 2 years ago

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.

rateofclimb2• 2 years ago

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! :)

williamstein3• 2 years ago

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

dogboat5• 2 years ago

There was a great documentary TV shown about this story.

baruz3• 2 years ago

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

tunesmith• 2 years ago

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.

euroderf2• 2 years ago

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

MrMcCall• 2 years ago

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

and we now know from AW's proof that the cubic and beyond fail.

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)

Each of the 4's go on the sides, and the 1 goes on the corner, leaving a pure 5x5 square left over.

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

jovas• 2 years ago

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.

sam_goody• 2 years ago

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.

hughesjj6• 2 years ago

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

j16sdiz2• 2 years ago

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

blackenedgem• 2 years ago

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

jebarker2• 2 years ago

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?

practal2• 2 years ago

Yes.

zozbot2348• 2 years ago

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.

jebarker2• 2 years ago

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.

ted_dunning3• 2 years ago

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.

charlieyu1• 2 years ago

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

levn11• 2 years ago

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

Tainnor9• 2 years ago

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.

digama03• 2 years ago

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.

Tainnor9• 2 years ago

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.

naasking9• 2 years ago

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

euroderf2• 2 years ago

Next target: the Langlands program ?

ThomasBb• 2 years ago

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_

le-mark• 2 years ago

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/

Fermat's Last Theorem – how it’s going

Related Stories