[HN Gopher] Fermat's Last Theorem - how it's going
___________________________________________________________________
Fermat's Last Theorem - how it's going
Author : verbify
Score : 412 points
Date : 2024-12-12 14:30 UTC (2 days ago)
(HTM) web link (xenaproject.wordpress.com)
(TXT) w3m dump (xenaproject.wordpress.com)
| munchler wrote:
| > 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 wrote:
| Compilers have this very same habit!
| munchler wrote:
| Yes. In fact, Lean is a compiler and type checkers are
| theorem provers (by the Curry-Howard correspondence). Proofs
| are programs!
| dboreham wrote:
| And Mathematics is Computer Science. Took me most of a
| lifetime to realize this.
| pkoird wrote:
| I'd argue for the converse: Computer Science is
| Mathematics
| practal wrote:
| 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.
| hughesjj wrote:
| Then we have the ghosts of information and category
| theories underpinning/influencing them all (including
| physics) (to some degree)
| naasking wrote:
| > 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.
| anthk wrote:
| 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
| gedpeck wrote:
| 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?
| jerf wrote:
| 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.
| gedpeck wrote:
| 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.
| immibis wrote:
| why should computer science be limited to things that are
| first order PA?
| gedpeck wrote:
| 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?
| naasking wrote:
| > 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.
| gedpeck wrote:
| The set of statements about natural numbers that are
| true.
| naasking wrote:
| 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.
| Tainnor wrote:
| 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).
| naasking wrote:
| 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?
| Tainnor wrote:
| Yes because the existence of a basis for arbitrary vector
| spaces is _equivalent to_ the axiom of choice.
| naasking wrote:
| A derivation of the axiom of choice in Martin-Lof 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.
| zozbot234 wrote:
| > 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.
| naasking wrote:
| 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.
| zozbot234 wrote:
| 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.)
| hughesjj wrote:
| 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.
| semolinapudding wrote:
| 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.
| gedpeck wrote:
| 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.
| semolinapudding wrote:
| 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 Godel'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 Godel '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...
| gedpeck wrote:
| You know more than me on logic so I defer to your
| expertise.
|
| https://math.stackexchange.com/questions/4753432/g%C3%B6d
| els...
|
| 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...
| Tainnor wrote:
| > 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)
| gedpeck wrote:
| 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.
| semolinapudding wrote:
| 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!), Godel'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.
| gedpeck wrote:
| Thanks for the reply.
| Tainnor wrote:
| > 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.
| gedpeck wrote:
| 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%B6d
| els...
| Tainnor wrote:
| > Take the collection of all true statements and make
| that your axiomatic system.
|
| A complete proof system needs to be able to derive G |-
| ph for _every_ pair G, ph such that G |= ph. Not just
| when G 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.
| gedpeck wrote:
| 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.
| Tainnor wrote:
| > 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). Godel's proof itself doesn't
| directly work for second-order logic. But the statement
| "if G is some axiomatic system that satisfies certain
| conditions, then for any sound proof calculus there is a
| sentence that isn't provable from G 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.
| gedpeck wrote:
| 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.
| Tainnor wrote:
| 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 Lowenheim-
| 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".
| Vt71fcAqt7 wrote:
| >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?
| justincredible wrote:
| Would it take too long or is it just that the margin is
| too small?
| pennomi wrote:
| I'm happy to see so much work going into fixing human errors in
| mathematics in a rigorous way.
| seanwilson wrote:
| > 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 wrote:
| > 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 wrote:
| 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-whale wrote:
| > 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.
| jmpetroske wrote:
| The reason Hilbert failed is because it's mathematically
| impossible (Godels incompleteness theorem).
| ur-whale wrote:
| > because it's mathematically impossible
|
| I guess the Lean devs can all pack and go home then.
| Also: how could they possibly miss Godel's theorem, how
| careless of them.
| jmpetroske wrote:
| 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.
| lambdaone wrote:
| While it's true that mathematics cannot ever be _completely_
| formalized, per Godel '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".
| tialaramex wrote:
| 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 Godel 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.
| youoy wrote:
| 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.
| lisper wrote:
| 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.
| j16sdiz wrote:
| 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.
| paulddraper wrote:
| > While it's true that mathematics cannot ever be
| completely formalized, per Godel'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.
| zozbot234 wrote:
| 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.)
| naasking wrote:
| > 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_rider wrote:
| 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 wrote:
| [flagged]
| analog31 wrote:
| While true, there are some clues such as the correlation
| between someone's occupation and their IQ.
| bee_rider wrote:
| I just meant in the context of math skills, but I definitely
| acknowledge that it was poor phrasing on my part.
| dogboat wrote:
| 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.
| TechDebtDevin wrote:
| 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.
| dogboat wrote:
| Maybe less coffee :)
| hughesjj wrote:
| But how else would I power this machine that outputs
| theorems?
| dogboat wrote:
| Erdos found stronger drugs
| NooneAtAll3 wrote:
| become comathematician and turn cotheorems into ffee
| dang wrote:
| 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
| dang wrote:
| " _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-whale wrote:
| > 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_rider wrote:
| 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.
| boothby wrote:
| 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 wrote:
| 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 wrote:
| 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
| staunton wrote:
| 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 wrote:
| That's such a nice way to think about unit tests! (In this
| context and others.)
| ur-whale wrote:
| 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 wrote:
| This makes me wonder if there'll ever be a significant bug
| discovered in Lean itself, breaking past formalisation work.
| pkoird wrote:
| Ahh, so maybe we should first focus on formalizing Lean itself?
| digama0 wrote:
| Should I introduce you to https://arxiv.org/abs/2403.14064 ?
| moomin wrote:
| 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.
| munchler wrote:
| 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
| digama0 wrote:
| 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.
| vouaobrasil wrote:
| > 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 wrote:
| 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 wrote:
| 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.
| moomin wrote:
| Baker's little book of number theory made me work to get
| through every page...
| inglor_cz wrote:
| 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 wrote:
| 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 wrote:
| 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.
| hughesjj wrote:
| 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
| impendia wrote:
| 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.
| vouaobrasil wrote:
| > 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.
| jll29 wrote:
| 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.
| ykonstant wrote:
| 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.
| robinzfc wrote:
| 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.
| zozbot234 wrote:
| 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.
| ykonstant wrote:
| 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.
| impendia wrote:
| 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.
| ykonstant wrote:
| > (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.
| zellyn wrote:
| 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.
| joe_the_user wrote:
| _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.
| adrian_b wrote:
| 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.
| XorNot wrote:
| 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.
| smj-edison wrote:
| 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.
| jll29 wrote:
| DOIs fix that.
| plank wrote:
| 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.
| zozbot234 wrote:
| > 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.
| impendia wrote:
| 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.
| zozbot234 wrote:
| 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.
| brap wrote:
| >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.
| dogboat wrote:
| I didn't learn big O at high school though.
| wbl wrote:
| Calc AB covers it, and BC certainly gives you enough for a
| proof.
| NooneAtAll3 wrote:
| "the proof is trivial"
|
| "but can you prove it?
|
| [10 minutes of intense staring and thinking]
|
| "yes, it is trivial"
| rstuart4133 wrote:
| > 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.
| zozbot234 wrote:
| > 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.
| eab- wrote:
| > 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)
| ykonstant wrote:
| 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.
| panda-giddiness wrote:
| 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...
| devit wrote:
| 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'Hopital's rule, differentiation
| algorithms and well-known limits at infinity).
| bandrami wrote:
| 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.
| nicf wrote:
| 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.
| rocqua wrote:
| 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 wrote:
| 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.
| jsvlrtmred wrote:
| 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.
| imprime wrote:
| 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.
| wbl wrote:
| 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.
| LegionMammal978 wrote:
| 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.
| rendaw wrote:
| 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 wrote:
| > 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/ )
| paulddraper wrote:
| 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 wrote:
| Yes, famously the Italian school of algebraic geometry ran
| into foundational issues. See https://en.wikipedia.org/wiki/I
| talian_school_of_algebraic_ge....
| boothby wrote:
| 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-cot wrote:
| > 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 wrote:
| > 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 wrote:
| 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_lurker wrote:
| > 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.
| baruz wrote:
| > 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.
| bell-cot wrote:
| 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. ...
| gjm11 wrote:
| 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.
| bell-cot wrote:
| > 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.
| subsistence234 wrote:
| 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).
| mostly_a_lurker wrote:
| > 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).
| baruz wrote:
| 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
| XorNot wrote:
| 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.
| lmm wrote:
| 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.
| CJefferson wrote:
| 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.
| brendanyounger wrote:
| 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.
| williamstein wrote:
| 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.
| boothby wrote:
| > 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.
| setopt wrote:
| > my foray into superconducting circuit design
|
| Curious, what do you work on? (I also research
| superconductivity.)
| boothby wrote:
| 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!
| cha42 wrote:
| Recently I found myself happy to find bug in code I have
| writtdn for those reasons.
| awanderingmind wrote:
| > [...]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 wrote:
| > 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?
| naasking wrote:
| Surely there was angry muttering.
| boothby wrote:
| 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.
| NL807 wrote:
| Perhaps a chair tipped over at most.
| graycat wrote:
| 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 wrote:
| 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.
| ykonstant wrote:
| 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 wrote:
| 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 wrote:
| 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.
| ykonstant wrote:
| 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 wrote:
| > 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?
| staunton wrote:
| This has happened before, see, e.g. the biography of Vladimir
| Voevodsky. Spoiler: the world kept spinning.
| moomin wrote:
| Russell's paradox did the same thing. They had to go back to
| the drawing board.
| bubblyworld wrote:
| 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 =)
| rocqua wrote:
| 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 wrote:
| 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.
| moomin wrote:
| 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.
| rateofclimb wrote:
| 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! :)
| williamstein wrote:
| I took that class with you! It was amazing. Here are my
| notes: https://wstein.org/books/ribet-stein/
| williamstein wrote:
| 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=IwZ
| Xh0bgNhZW0CM...
| rateofclimb wrote:
| Thanks for sharing that! Very cool.
| dogboat wrote:
| There was a great documentary TV shown about this story.
| baruz wrote:
| 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 wrote:
| 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.
| euroderf wrote:
| Perhaps more delightful to the ears to hear that a proof has
| been disemboweled.
| MrMcCall wrote:
| 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 wrote:
| 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 wrote:
| 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.
| hughesjj wrote:
| 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
| j16sdiz wrote:
| 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
| hughesjj wrote:
| 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)
| blackenedgem wrote:
| You may want to watch this if Surely You're Joking read years
| ago is your main reference point: https://youtu.be/TwKpj2ISQAc
| jebarker wrote:
| 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?
| practal wrote:
| Yes.
| zozbot234 wrote:
| 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.
| jebarker wrote:
| 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.
| charlieyu1 wrote:
| What is the simplest proof of FLT these days? I don't think
| elementary proofs exist
| levn11 wrote:
| https://www.techrxiv.org/users/717330/articles/702287-on-fer...
| Tainnor wrote:
| 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.
| digama0 wrote:
| 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.
| Tainnor wrote:
| 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.
| naasking wrote:
| Nice story, and I'm glad formalization work is proceeding.
| "Details left as an exercise to the reader" is the bane of true
| knowledge.
| euroderf wrote:
| Next target: the Langlands program ?
| ThomasBb wrote:
| 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 wrote:
| 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/
___________________________________________________________________
(page generated 2024-12-14 23:01 UTC)