[HN Gopher] Mathematicians welcome computer-assisted proof in 'g...
___________________________________________________________________
Mathematicians welcome computer-assisted proof in 'grand
unification' theory
Author : Wxc2jjJmST9XWWL
Score : 212 points
Date : 2021-06-19 12:33 UTC (10 hours ago)
(HTM) web link (www.nature.com)
(TXT) w3m dump (www.nature.com)
| mjreacher wrote:
| Is there any opportunity for interested undergrads to learn about
| this more (since I doubt we could contribute)?
| foooobar wrote:
| If you're interested in interactive theorem proving with Lean
| (and not condensed mathematics), the Lean community landing
| page is a good place to start. https://leanprover-
| community.github.io/
|
| Especially the "Natural Number Game" under "Learning resources"
| has been successful in teaching folks the very basics for
| writing proofs. Once finished, a textbook like "Theorem Proving
| in Lean" can teach the full basics. Feel free to join the Lean
| Zulip at any point and ask questions at
| https://leanprover.zulipchat.com/ in the #new members stream.
|
| Mathlib has plenty of contributions from interested undergrads
| :)
| Tainnor wrote:
| This is going to be an exciting area.
|
| I spent some time previously playing with Coq. It's very
| powerful, but even proving the simplest undergraduate maths
| statements (say, about group theory) can prove very challenging.
| I believe that part of this is that Coq uses different
| mathematical foundations than traditional mathematics, which
| mostly uses set theory (ZFC, although most people don't care
| about the specifics). So it can be hard or unnatural to express
| something like "subgroup". I don't know if Lean fares better in
| that respect. Coq documentation is also IMHO almost impossible to
| understand unless you're already very deeply knowledgeable about
| the system.
|
| We will probably still need some more iterations, to get more
| user friendly assistants with better documentation and to get
| adequate teaching resources etc.
| ixaxaar wrote:
| Hey type hacking is hard. Agda is kinda easier for someone who
| knows haskell, but hard nonetheless.
| deadbeef57 wrote:
| In my experience, the difficulty is very rarely the transition
| from set theory to type theory. I find this almost transparent
| in practice.
|
| The issue is rather that you need to deal with edge cases that
| are usually swept under the rug, or that you need to spend a
| full page working out the details of a proof that everyone
| recognizes as obvious. It would be great if computers could
| give even more assistance with these tedious parts of
| formalization, and I'm very glad that people are working hard
| on realizing this.
| ganzuul wrote:
| Kurt Godel with a bat in dark alleyway of obviousness haunts
| my dreams.
| raphlinus wrote:
| Lean's foundations are similar to Coq. I think the ergonomics
| are a bit better.
|
| Most activity in proof systems is based in type theory these
| days, but set theoretical systems do exist, of which Metamath
| is the most mature. That said, Metamath is seriously lacking in
| automation, so there is an element of tedium involved. That's
| not because of any fundamental limitations, but I think mostly
| because people working in the space are more motivated to do
| things aligned with programming language theory. There was also
| a talk by John Harrison a few years ago proposing a fusion of
| HOL and set theory, but I'm not sure there's been much motion
| since then.
|
| I believe a fully featured proof assistant based in set theory
| would be a great contribution.
|
| [1]: http://aitp-conference.org/2018/slides/JH.pdf
| Ericson2314 wrote:
| You don't need subgroups, you just need injective
| homomorphisms.
| zozbot234 wrote:
| ZFC was only ever developed as a proof of concept, not as a
| practical foundation for formal math. Structural set theories,
| type theories or category-based foundations are actually a lot
| easier to work with, and otherwise quite equivalent in power.
| Tainnor wrote:
| This is missing the point. Modern mathematics textbooks,
| especially undergratuate ones, are written with set theoretic
| foundations. It requires a lot of effort to reformulate all
| of mathematics into equivalent formulations. That makes it
| harder to get buy-in from many working mathematicians, and it
| also makes the subject less approachable for, say,
| undergraduates.
| zozbot234 wrote:
| Modern math textbooks are based on naive set theory, which
| can be quite feasibly modeled, even by structural
| foundations. It might require _some_ effort at the lowest
| layer of formalization, but even then only as a one-time
| thing that 's not going to impact the project as a whole.
| Tainnor wrote:
| That may very well be the case, but to a person starting
| out right now, those foundations seem to be lacking right
| now (or at least are not easily discoverable).
| xvilka wrote:
| Interesting choice of the proof assistant though - some specific
| parts of the Lean's core are not completely decidable, moreover
| the upcoming Lean 4 version is incompatible with many libraries
| and proofs written for Lean 3. See also the discussion[1] if the
| Coq is suitable for number theory as quotients are ubiquitous
| here.
|
| [1] https://github.com/coq/coq/issues/10871
| generationP wrote:
| As to decidability: I suspect you mean that Lean's foundations
| are non-constructive. I'd rather they weren't, but with what
| Peter Scholze is doing, I'd be surprised if the arguments could
| be made constructive within just a few years from their
| conception. This usually takes much longer (e.g., constructive
| proofs of the Quillen-Suslin theorem appeared in print just a
| few years ago).
|
| About incompatibility: Last time I checked (some 3 or so years
| ago), Coq was not backwards compatible either, and libraries
| had to be ported manually with each update. Sadly, as this is
| the one greatest anti-feature that is currently putting me off
| proof assistants, but probably it needs some time, and the
| quickest way to get there is to maximize usage. From what I
| know about Coq and Lean, I suspect Lean will stabilize faster
| than Coq does, due to it being more "declarative" (Coq is based
| too much on complex tactics, which are hard to make stable by
| design).
| ulber wrote:
| I wasn't aware of Lean not being sound and a quick search
| didn't come up with anything related to that. Could you link a
| source?
| martincmartin wrote:
| See other comment. It's sound but not decidable.
| kevinbuzzard wrote:
| Basically it turned out that theoretical undecidability did
| not matter in practice, because Scholze mathematics relies
| so little on definitional equality. We prove theorems with
| `simp` not `refl`. Pierre-Marie Pedrot is quoted above as
| saying that various design decisions are "breaking
| everything around", but we don't care that our `refl` is
| slightly broken because it is regarded as quite a low-level
| tool for the tasks (eg proving theorems of Clausen and
| Scholze) that we are actually interested in, and I believe
| our interests contrast quite a lot with the things that
| Pedrot is interested in.
| bryan0 wrote:
| Can you explain to a non-mathematician how you can prove
| anything without refl (which I assume is the statement
| "x=x is true") ?
| digama0 wrote:
| The jargon is a bit confusing sometimes. In Lean, "refl"
| does a whole lot more than prove x=x. It is of course
| available if you want to prove x=x, but the real power of
| "refl" is that it also proves x=y where x and y are
| definitionally equal. Or at least that's the idea; it
| turns out that lean's definitional equality relation is
| not decidable so sometimes it will fail to work even when
| x and y are defeq, and this is the theoretically
| distasteful aspect that came up on the linked Coq issue.
| In practice, the theoretical undecidability issue never
| happens, however there is a related problem where
| depending on what is unfolded a proof by "refl" can take
| seconds to minutes, and if alternative external proof-
| checkers don't follow exactly the same unfolding
| heuristics it can turn a seconds long proof into a
| thousand-year goose chase. By comparison, methods like
| "simp" have much more controllable performance because
| they actually produce a proof term, so they tend to be
| preferable.
| kmill wrote:
| And in "Lean style", refl proofs are a bit distasteful
| from a software engineering point of view because they
| pierce through the API of a mathematical object. (In the
| language of OOP, it can break encapsulation.)
|
| It tends to be a good idea to give _some_ definition,
| then prove a bunch of lemmas that characterize the
| object, and finally forget the definition.
| deadbeef57 wrote:
| The claim that Lean's core is not completely sound is FUD.
| Completely bogus.
|
| You might be confused by the fact that Lean's definitional
| equality is not decidable, but that doesn't mean it isn't
| sound. Nobody has ever found a proof of `false` so far in Lean
| 3.
|
| The choice for Lean is actually quite natural: (i) it has a
| large and _coherent_ library of mathematics to build such a
| project upon. And (ii), it has a substantial user base of
| mathematicians somewhat familiar with the subject at hand
| (i.e., condensed mathematics).
|
| The initial challenge by Peter Scholze was directed at all
| theorem proving communities. As far as I know, only the Lean
| community took up the challenge.
|
| (Concerning Lean 4: yes, mathlib will have to be ported. And
| yes, people are working hard on this. I think that none of the
| theorem provers so far are ready for wide-scale use in
| mathematics. And that's why it is important to iterate fast.
| The Lean community is not afraid of redesigns and large
| refactors when discovering better approaches.)
| kzrdude wrote:
| Shouldn't it be easy to automatically port theorems? If they
| are well defined there can't be ambiguity
| deadbeef57 wrote:
| Yes and no. If you want to port large low-level proof
| objects in all their gory detail, then this has been done
| already. But if you want to port the more concise higher-
| level proof scripts you run in all the same issues as with
| regular transpilers.
|
| Compare it to porting machine code for one instruction set
| to another instruction set. This is usually doable in a
| straightforward manner (maybe with a mild performance
| penalty). But transpiling idiomatic Java to idiomatic
| Haskell is nigh impossible.
|
| Luckily, the differences between Lean 3 and Lean 4 are not
| as large as between Java and Haskell. But still, they have
| different idioms, different syntax, different features. And
| this has to be taken care of.
| Someody42 wrote:
| In theory yes, but there are two main things that makes it
| harder :
|
| - some technical details have changed. They don't affect
| the axiomatic aspects of Lean, but they force us to
| redefine some things in a cleaner way.
|
| - we don't only want to port the theorem. We want to port
| them to a human-readable proof that can be easily
| maintained
| xvilka wrote:
| > You might be confused by the fact that Lean's definitional
| equality is not decidable, but that doesn't mean it isn't
| sound. Nobody has ever found a proof of `false` so far in
| Lean 3.
|
| You are right, my bad. Taking my words back on that.
|
| A bit more details from the Pierre-Marie Pedrot:
|
| > Lean does not escape this limitation, as it defines the
| equality type inductively as in Coq. Rather, in a mastermind
| PR campaign, they successfully convinced non-experts of type
| theory that they could give them quotient types without
| breaking everything around.
|
| > The first thing they do is to axiomatize quotient types,
| which is somewhat fine and can be done the same in Coq. As
| any use of axioms, this breaks canonicity, meaning your
| computations may get stuck on some opaque term. (While
| slightly cumbersome, axiomatizing quotients already solves
| 99,9% of the problems of the working mathematician).
|
| > Now, were they do evil things that would make decent type
| theorists shake in terror, they add a definitional reduction
| rule over the quotient induction principle. We could do the
| same in the Coq kernel, but there is a very good reason not
| to do this. Namely, this definitional rule breaks subject
| reduction, which is a property deemed more important than
| loss of canonicity.
|
| > In Lean, you can write a term t : A where t reduces to u,
| but u doesn't have type A (or equivalently may not typecheck
| at all). This is BAD for a flurry of reasons, mark my words.
| Reinstating it while keeping quotients requires an
| undecidable type checking algorithm, which is another can of
| worms you don't want to wander into. The same kind of trouble
| arises from similar Lean extensions like choice.
| deadbeef57 wrote:
| > Lean does not escape this limitation, as it defines the
| equality type inductively as in Coq. Rather, in a
| mastermind PR campaign, they successfully convinced non-
| experts of type theory that they could give them quotient
| types without breaking everything around.
|
| This is not the first time that I hear someone from the Coq
| community talk about Lean and its "mastermind PR campaign".
| To me it comes across in a denigrating way, and frankly I'm
| a bit sick of it.
|
| Working mathematicians are usually not experts of type
| theory. Yes. But they aren't stupid either. Why does the
| Lean community have such a large number of mathematician
| users? Why did it successfully formalize the main technical
| result of Peter Scholze's challenge in less than 6 months?
| Is this all because of a "mastermind PR campaign" selling
| mathematicians snake oil?
|
| There has been some strong disagreements and even mud
| slinging between the Coq and Lean communities in the past.
| But I thought that axe was buried. I would like to move on.
|
| I'm fine with people finding the foundations of Lean ugly,
| distasteful, improper, or whatever. But please stop the
| insults.
| zozbot234 wrote:
| The Coq folks tend to focus on constructivity, and Lean
| gets sold as a constructive system but then you get this
| weird axiomatised-quotients stuff that's the farthest
| thing from constructivity. I can see how they might find
| that kind of thing highly frustrating.
|
| It might not show up as a problem if you only ever care
| about classical stuff, but there are arguably better ways
| of doing purely classical mathematics that don't
| arbitrarily break interoperability w/ the constructive
| world.
| deadbeef57 wrote:
| Where does Lean get sold as a constructive system?
| Certainly mathlib (the main maths library in Lean) is
| very upfront about being classical.
| zozbot234 wrote:
| mathlib != Lean. I'm talking about the basic logic.
| People will try to sell you Lean by describing its system
| as constructive, but if so the quotients stuff is pure
| breakage as the Coq folks point out.
|
| And if Lean could support classical logic without
| arbitrarily breaking interop for folks who want to _also_
| prove constructive statements, we might see some
| additions to mathlib with a closer focus on constructive
| math.
| foooobar wrote:
| I don't think anyone is trying to sell Lean as a
| constructive system. The current developers certainly
| don't think of it that way, further evidenced by the fact
| that the typical way of doing computation in Lean does
| not involve definitional reduction, but using `#eval`
| with additional low level code for performance. Proof
| irrelevance (and quotients) were adopted with that in
| mind.
| Someody42 wrote:
| You can absolutely do constructive things in Lean, as
| long as you use neither the built-in "quot" type nor the
| three other axioms described in the docs, and then you
| get a system with all the desired properties I think
| foooobar wrote:
| Some constructivists may also take offense with proof
| irrelevance (and the resulting loss of normalization [1]
| or its incompatibility with HoTT), which you can only
| really avoid by avoiding Prop.
|
| [1] https://arxiv.org/abs/1911.08174
| deadbeef57 wrote:
| I agree very much that mathlib != Lean. Still, I think
| much of the talk about Lean will mention that mathlib is
| classical.
|
| It was an honest question: I don't know where Lean is
| sold as a constructive system. (Note, I haven't read
| every part of Lean's documentation or website. I might be
| missing something obvious here.)
| deadbeef57 wrote:
| Ok, no worries. I understand that from a theoretical point
| it's not so nice that defeq is not decidable. But frankly I
| don't care. Because in practice, I don't know of any
| example where someone was bitten by this. It only shows up
| in contrived examples. And even if you have some practical
| example where lean gets stuck on A = B, it will probably be
| very easy to find a C so that lean gets unstuck on A = C =
| B.
|
| [Edit, this comment only replies to the first paragraph of
| parent. I wrote it before parent was edited.]
| xvilka wrote:
| By the way, just for the record, I like many aspects of
| the new Lean 4 design and wish the project luck. They
| really aim for better maintainability and user
| experience. It is nice to see them taking best solutions
| from other programming languages and frameworks.
| qntmfred wrote:
| A quick intro from quanta magazine to Kevin Buzzard's work on
| computer-assisted proof systems
|
| https://www.youtube.com/watch?v=HL7DEkXV_60&t=295s
| FabHK wrote:
| TIL: Fields medallists ask questions on MathOverflow... [1]
|
| This has me in awe about the depth of mathematics, the pace of
| progress, the miracle of specialisation. I have a degree in an
| applied-math-y adjacent field, and understand nothing. (And, btw,
| I was astonished how knowledgable some commenters right here
| were, and then realised that we have the (co-)authors of the
| results themselves here! gotta love HN.)
|
| With that said, here some (non-mathematical) snippets I found
| interesting (apart from the great word "sheafification"):
|
| > Why do I want a formalization?
|
| > -- I spent much of 2019 obsessed with the proof of this
| theorem, almost getting crazy over it. In the end, we were able
| to get an argument pinned down on paper, but I think nobody else
| has dared to look at the details of this, and so I still have
| some small lingering doubts.
|
| > -- while I was very happy to see many study groups on condensed
| mathematics throughout the world, to my knowledge all of them
| have stopped short of this proof. (Yes, this proof is not much
| fun...)
|
| > -- I have occasionally been able to be very persuasive even
| with wrong arguments. (Fun fact: In the selection exams for the
| international math olympiad, twice I got full points for a wrong
| solution. Later, I once had a full proof of the weight-monodromy
| conjecture that passed the judgment of some top mathematicians,
| but then it turned out to contain a fatal mistake.)
|
| > -- I think this may be my most important theorem to date. (It
| does not really have any applications so far, but I'm sure this
| will change.) Better be sure it's correct...
|
| > In the end, one formulates Theorem 9.5 which can be proved by
| induction; it is a statement of the form [?][?][?][?][?][?]
| (\forall \exists \forall \exists \forall \exists), and there's no
| messing around with the order of the quantifiers. It may well be
| the most logically involved statement I have ever proved.
|
| > Peter Scholze, 5th December 2020 [2]
|
| Question: What did you learn about the process of formalization?
|
| Answer: I learnt that it can now be possible to take a research
| paper and just start to explain lemma after lemma to a proof
| assistant, until you've formalized it all! I think this is a
| landmark achievement.
|
| Question: And about the details of it?
|
| Answer: You know this old joke where a professor gets asked
| whether some step really is obvious, and then he sits down for
| half an hour, after which he says "Yes, it is obvious". It turns
| out that computers can be like that, too! Sometimes the computer
| asks you to prove that A=B, and the argument is "That's obvious
| -- it's true by definition of A and B." And then the computer
| works for quite some time until it confirms. I found that really
| surprising.
|
| Question: Was the proof in [Analytic][4] found to be correct?
|
| Answer: Yes, up to some usual slight imprecisions.
|
| Question: Were any of these imprecisions severe enough to get you
| worried about the veracity of the argument?
|
| Answer: One day I was sweating a little bit. Basically, the proof
| uses a variant of "exactness of complexes" that is on the one
| hand more precise as it involves a quantitative control of norms
| of elements, and on the other hand weaker as it is only some kind
| of pro-exactness of a pro-complex. It was implicitly used that
| this variant notion behaves sufficiently well, and in particular
| that many well-known results about exact complexes adapt to this
| context. There was one subtlety related to quotient norms -- that
| the infimum need not be a minimum (this would likely have been
| overlooked in an informal verification) -- that was causing some
| unexpected headaches. But the issues were quickly resolved, and
| required only very minor changes to the argument. Still, this was
| precisely the kind of oversight I was worried about when I asked
| for the formal verification.
|
| Question: Were there any other issues?
|
| Answer: There was another issue with the third hypothesis in
| Lemma 9.6 (and some imprecision around Proposition 8.17); it
| could quickly be corrected, but again was the kind of thing I was
| worried about. The proof walks a fine line, so if some argument
| needs constants that are quite a bit different from what I
| claimed, it might have collapsed.
|
| Question: Interesting! What else did you learn?
|
| Answer: What actually makes the proof work! When I wrote the blog
| post half a year ago, I did not understand why the argument
| worked, and why we had to move from the reals to a certain ring
| of arithmetic Laurent series. [...]
|
| Question: So, besides the authors of course, who understands the
| proof now?
|
| Answer: I guess the computer does, as does Johan Commelin. [Note:
| = deadbeef57 here on HN][3]
|
| [1] https://mathoverflow.net/questions/386796/nonconvexity-
| and-d...
|
| [2] https://xenaproject.wordpress.com/2020/12/05/liquid-
| tensor-e...
|
| [3] https://xenaproject.wordpress.com/2021/06/05/half-a-year-
| of-...
|
| [4] http://www.math.uni-bonn.de/people/scholze/Analytic.pdf
| Barrin92 wrote:
| The abiltiy to automate proofs creates some interesting questions
| about the nature of mathematics. The article remined me of Erdos
| saying that you "don't need to believe in God, but you do need to
| believe in the book", 'the book' here being an imagined
| collection of mathematical proofs that are so simple, clear and
| beautiful that they immedieately stand out to any mathematician.
|
| I don't mind proof assistants as a way to gain new insights into
| mathematics, but I worry that maths is drifting into a direction
| where it turns more into hermeneutics than actual mathematics.
| The automation of proofs isn't the only thing, I also was very
| scpetical about the whole process of Shinichi Mochizuki's proof
| of the abc conjecture.
| civilized wrote:
| Automated proofs aren't remotely comparable to Mochizuki's abc
| stuff. Automated proofs just handle a lot of complicated case
| by case checking that humans could in principle do, it's just
| too much work, like counting to a trillion. Automated proof
| systems are incapable of the brilliant but unreliable intuitive
| leaps that mathematicians can make.
|
| Mochizuki's stuff is simply a hypercomplicated pile of nonsense
| unintelligible to the mathematical community.
| deadbeef57 wrote:
| As explained in another comment, there is only very mild proof
| automation going on in this Lean project. Every non-trivial
| idea has to be supplied to the computer by a human being.
|
| The whole circus around Mochizuki's proof of the abc conjecture
| was dealt with quite well by the social structure of the
| mathematical community. Many people looked at the proof. Many
| people got stuck. Several experts got stuck at exactly the same
| point. And Mochizuki refuses to acknowledge that there is a
| problem at that point of his "proof". But a consensus was
| reached in the mathematical community (maybe minus RIMS).
| kungito wrote:
| What's the name of this point? It's really hard to find any
| progress on this topic regarding Mochizuki other than some
| popular articles without any content.
| deadbeef57 wrote:
| See https://www.math.columbia.edu/~woit/wordpress/?p=10560,
| which links to a technical write-up by Scholze and Stix
| about what they think is the issue with Mochizuki's proof.
| Woit's blogpost also gives a bit more links, including a
| response by Mochizuki.
| bryan0 wrote:
| The paper which everyone linked to when the discussion
| was going on now 404s, so here is a new link: https://nca
| tlab.org/nlab/files/why_abc_is_still_a_conjecture...
|
| The point in the proof where scholze and stix show it
| fails is "IUTT-3, Corollary 3.12"
| citrusynapse wrote:
| Made an account just to share this incredible book that follows
| Erdos's life & exploits:
|
| https://en.wikipedia.org/wiki/The_Man_Who_Loved_Only_Numbers
| inigojonesguy wrote:
| The article is only publicity for Scholze, looks to me as a
| remake of the same thing done for Cedric Villani. Old boys
| games behind fresh faces, ok boomer stuff.
| Ericson2314 wrote:
| On the contrary proof assistants help one systematize and
| organize existing concepts. They are a great way to revise the
| basic curriculum and revolutize pedagogy. They make the
| creative process of defining new mathematical objects more
| accessible, and easier to motivate via unlocking more code
| reuse. They are a great way to revise the basic curriculum and
| revolutize pedagogy.
| denial wrote:
| Does anyone know how condensed mathematics would fit into the
| modern theory of PDEs (which is heavily based on functional
| analysis)? Perhaps it's a relic of the sort of math Scholze works
| on, but it looks far too abstract to provide an impetus for
| people in those fields to embrace it. Topology, on the other
| hand, is relatively easy to define and work with (though there
| are some quirks with dual spaces of continuous linear functionals
| I've seen aesthetic objections to). Or does it "contain" topology
| in some sense, allowing people to continue working with notions
| of convergence obtained from norms?
| deadbeef57 wrote:
| I think that right now it is not clear why condensed/liquid
| mathematics would be useful for PDEs. On the other hand, your
| question
|
| > Or does it "contain" topology in some sense, allowing people
| to continue working with notions of convergence obtained from
| norms?
|
| has a positive answer. You can, if you want, swap out
| topological spaces, and use condensed sets instead, and just
| continue with life as usual.
|
| At the same time, all of this is in fast paced development, so
| hopefully we will see some killer apps in the near future. But
| I expect them more in the direction of Hodge theory and complex
| analytic geometry.
| wolverine876 wrote:
| Thanks for sharing your expertise. Would you be open to
| sharing your background? Obviously it's not required, but it
| would help contextualize what you're saying for the
| interested non-mathematician; otherwise we're kinda stuck
| with 'some guy on the Internet said ...' syndrome. :)
| deadbeef57 wrote:
| Sure, I just created an account a couple of days ago, and
| my favourite username was already taken :oops:
|
| I'm Johan Commelin, https://math.commelin.net/
| alimw wrote:
| Hi! Imagine for a moment that your next project required
| you to develop a lot of functional analysis and PDE
| theory in Lean. Would you be tempted to build that on top
| of what you've done (or will have done) with condensed
| sets?
| wolverine876 wrote:
| Thank you! And welcome! Make yourself at home.
| est wrote:
| is there a simpler version of LEAN suitable for high school
| student level math? Sympy?
| deadbeef57 wrote:
| You might enjoy
| http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game...
|
| It's a game implemented in lean, where you work your way
| through the basic facts about natural numbers.
| Tainnor wrote:
| sympy is not a proof assistant, but a symbolic computer algebra
| system
| lvh wrote:
| I recommend the following post, by the author of the proof, for
| deeper context. Especially near the end, they talk about some of
| the things they're trying to accomplish with it in plain(ish)
| English.
|
| https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...
| deadbeef57 wrote:
| See also [1] for a follow-up blogpost that is less technical.
|
| [1]: https://xenaproject.wordpress.com/2021/06/05/half-a-year-
| of-...
| ajarmst wrote:
| The article is interesting, but that lede is incoherent. Many
| mathematicians accept computer proofs the way chess grand masters
| accept computer players. Computer "assistants" that generate
| proofs that humans cannot follow or understand will always be
| controversial, and the proofs they generate, even though accepted
| as valid, will always be decorated with an asterisk.
| LudwigNagasena wrote:
| I don't understand the chess analogy. How is it in any way
| similar?
| kevinbuzzard wrote:
| Lean and the other theorem provers turn mathematical proofs
| into levels of a computer puzzle game, much like a chess
| puzzle.
| [deleted]
| 6gvONxR4sf7o wrote:
| If not an asterisk, they'll just have less impact. A proof
| generates a fact. The best facts and proofs are useful in that
| they help _other_ things. You work becomes useful for my work,
| which may become useful for others.
| kevinbuzzard wrote:
| Presumably the asterix denotes "actually true"? ;-)
| 363849473754 wrote:
| This is a proof assistant, not an automated theorem prover. The
| user has to supply* the mathematics and the proof checker
| formally verifies whether or not the steps are correct. It
| doesn't have any creativity (that's up to the mathematician).
|
| *I should have clarified there is some proof generation, see
| the comment below by opnitro, but I meant the meat and potatoes
| of novel non-trivial proofs currently has to be supplied by the
| user.
| ajarmst wrote:
| Thanks for the clarification.
| opnitro wrote:
| That's not quite true. Many of these proof assistants support
| some level of automation and proof search. I haven't used
| Lean specifically, but it's quite common in Coq for projects
| to write proof search techniques specific to the problem
| domain and utilize them in their proofs.
| gigatexal wrote:
| For anyone frustrated that the article doesn't say what specific
| part of math has the most to gain it's here:
|
| " The crucial point of condensed mathematics, according to
| Scholze and Clausen, is to redefine the concept of topology, one
| of the cornerstones of modern maths. A lot of the objects that
| mathematicians study have a topology -- a type of structure that
| determines which of the object's parts are close together and
| which aren't. Topology provides a notion of shape, but one that
| is more malleable than those of familiar, school-level geometry:
| in topology, any transformation that does not tear an object
| apart is admissible. For example, any triangle is topologically
| equivalent to any other triangle -- or even to a circle -- but
| not to a straight line.
|
| Topology plays a crucial part not only in geometry, but also in
| functional analysis, the study of functions. Functions typically
| 'live' in spaces with an infinite number of dimensions (such as
| wavefunctions, which are foundational to quantum mechanics). It
| is also important for number systems called p-adic numbers, which
| have an exotic, 'fractal' topology."
| fjfaase wrote:
| For more details about the actual proof, see: 'Blueprint for the
| Liquid Tensor Experiment'
|
| https://leanprover-community.github.io/liquid/index.html
| SneakyTornado29 wrote:
| Last time someone talked about automating proofs, a whole new
| field was invented (computer science)
| sabujp wrote:
| "Proof assistants can't read a maths textbook, they need
| continuous input from humans, and they can't decide whether a
| mathematical statement is interesting or profound -- only whether
| it is correct, Buzzard says. Still, computers might soon be able
| to point out consequences of the known facts that mathematicians
| had failed to notice, he adds."
|
| we're closer to this than people realize
| gwern wrote:
| It's worth noting that GPT-f already gets a big performance
| boost from pretraining on Arxiv etc
| (https://arxiv.org/pdf/2009.03393.pdf#page=7) despite those
| sources containing next to no Metamath or anything that looks
| like a raw Metamath proof, just regular natural language &
| LaTeX discussing math...
| GPerson wrote:
| Why do you say this?
| kevinbuzzard wrote:
| I'm not quite sure what you're asking about. I'm saying that
| we can't yet take the Wiles and Taylor-Wiles proof of
| Fermat's Last Theorem, feed it into a machine, and get a Lean
| proof of Fermat's Last Theorem.
| GPerson wrote:
| Hi Kevin,
|
| Yes, I was responding to the person who said "we're closer
| to this than people realize" hoping to learn what they had
| in mind.
| wolverine876 wrote:
| I think the GP might have been responding to the GGP, not
| to your statement in the article.
| amelius wrote:
| > we're closer to this than people realize
|
| At least give a proper reference to what you're alluding to,
| please.
|
| Also, closeness in AI has shown to be a misleading concept.
| gerdesj wrote:
| A reference you might like to note is in a response - that
| kevinblizzard bloke probably has a fair old handle on this
| stuff. Note how he is quoted throughout the article.
|
| This is about some pretty creative uses of computing in maths
| and bugger all to do with AI (whatever that is.)
|
| If you put enough blood, sweat and tears into codifying
| mathematical concepts into Lean, you can feed it a
| mathematical thingie and it can tell you if that thingie is
| correct within its domain of knowledge. If you get an "out of
| cheese error", you need to feed it more knowledge or give up
| and take up tiddlywinks.
|
| This explains Lean in terms I can understand:
| https://www.quantamagazine.org/building-the-mathematical-
| lib...
| kevinbuzzard wrote:
| I agree, but I think my statement is accurate today in 2021. I
| would love to see funds directed towards this sort of question.
| The big problem is that _at high level_ so so much is skipped
| over, and you still sometimes have to struggle to put
| undergraduate-level mathematics into Lean -- this is why UG
| maths is such a good test case.
| mherrmann wrote:
| Very nice to see you here Kevin. We never interacted but I do
| still remember a lecture you gave at Imperial in '06 where
| you filled in for Prof. Liebeck and started with Lemma 1: "I
| am not Professor Liebeck" ;-) Thank you for the nice memory
| and your important work on / with Lean.
| zozbot234 wrote:
| > The big problem is that at high level so so much is skipped
| over
|
| This is an issue, but there's an established practice of
| writing _formal sketches_ where the gaps in the proof are
| explicitly marked, and future tooling might bring ways to
| address these gaps once a full formal context is provided.
|
| One issue is that Lean has little or no support for
| declarative proof, which is by far the most natural setting
| for these "proof sketches", and also brings other advantages
| wrt. complex proofs. (Coq has the same issue; some code was
| written to support declarative proofs, but it was too buggy
| and bitrotted, so it got removed.)
| foooobar wrote:
| As far as I can tell, this is not quite true. Tactic proofs
| aside, you can also write functional term mode proofs and
| declarative "structured" proofs in the sense of Isar.
| Theorem Proving in Lean introduces that style, so most
| people who use Lean are familiar with it: E.g. https://lean
| prover.github.io/theorem_proving_in_lean/proposi...
|
| Additionally, even in tactic proofs you can use tactics
| like `have`, `suffices`, etc. to manipulate the structure
| of the proof and make subgoals explicit like you would
| usually do in the structured style. In practice, people in
| Lean still prefer imperative tactic proofs with the option
| to write in a structured/declarative style where
| reasonable. The full "structured" mode does not see much
| use, since it is quite verbose. As a result, Lean 4 will
| not support this style out of the box anymore, but you
| could still add it yourself using the macro system.
| Haga wrote:
| Can't usefulness be approximated like Google search results of
| old, by connectedness to other theories.
___________________________________________________________________
(page generated 2021-06-19 23:00 UTC)