[HN Gopher] Formalizing the proof of PFR in Lean4 using Blueprin...
___________________________________________________________________
Formalizing the proof of PFR in Lean4 using Blueprint: a short tour
Author : georgehill
Score : 59 points
Date : 2023-12-05 09:19 UTC (13 hours ago)
(HTM) web link (terrytao.wordpress.com)
(TXT) w3m dump (terrytao.wordpress.com)
| lanstin wrote:
| Ok, I'll download lean4 and read the tutorials. Everything else
| I've tried that Prof. Tao has suggested has worked well. I didn't
| really realize that proof software had advanced so far. I tried
| to do a project in undergrad to put a lot of ZFC into Prolog but
| it was just too early to work.
| swagmoney1606 wrote:
| Lean4 has been a pleasure to learn so far! Starting with the
| natural numbers game was great for me:
| https://adam.math.hhu.de/
| Epa095 wrote:
| In the last comment below he writes
|
| > The project has now completed its primary goals; the entire
| dependency graph is now green.
| haskellandchill wrote:
| I don't follow how the proof text is generated from lean? Or is
| it not, they are doing the verification in lean and the proof
| text is completely separate.
|
| Looking at the project more I see it's the latter. Turning lean
| tactics into readable proof text would be hard, as the lean
| phrase book he is keeping shows:
| https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6...
| empath-nirvana wrote:
| There will probably be a time where most proofs are just done
| in Lean or some similar system and nobody bothers writing a
| "human readable" paper. Math will just become a kind of
| programming.
| 082349872349872 wrote:
| I had been under the impression that mechanised proof
| assistants were much too low level for actual mathematicians
| (like asking programmers to explicitly allocate functional
| units and issue slots?) so it's interesting news that Prof.
| Tao finds mucking about with them worthwhile.
| Someone wrote:
| From what I understand, it's more like requiring each
| programmer to write implementations of arrays,
| dictionaries, date/time handling code, float parsing and
| printing, etc.
|
| Once the language designers had figured out the hardware
| was now capable enough to make libraries useful, it only
| took one programmer to do that tedious work. After that all
| other programmers could reuse that work.
|
| This will be similar: once a large body of definitions and
| proofs has been built, mathematicians will be able to reuse
| higher-level constructs to build proofs for their theorems.
|
| It likely also will be similar in that there will be
| multiple approaches to this with one (or a few; it could be
| that one system works best/will have the largest set of
| definitions for one branch of mathematics, while another
| 'wins' in another) ending up victorious.
| t_mann wrote:
| Exactly. There are multiple ongoing projects to formalize
| existing math, there seems to be some convergence on
| Lean4 at the moment, but the best analogy is probably
| programming languages, where there's a constant battle
| between the old guards with huge staying power and newer
| entrants with just too many good ideas to ignore. Except
| that here a lot of the attractiveness of a language will
| come from how much math has been formalized in that
| language, which gives a huge advantage to the early
| leaders. So there might be a bit more emphasis on
| 'superset-languages' like Kotlin or TypeScript here, that
| can make use of the libraries from existing languages.
| lanstin wrote:
| I'm taking a masters in mathematics, and for me the steps are
| at least three-fold: understanding what you are trying to
| prove, which is mostly thinking about it and maybe reading or
| talking to people; picking up pen and paper and proceeding
| with a sketch of the essential points; typing the proof into
| LaTeX for a human readable homework :)
|
| I suspect lean will change the thoughts a bit but not
| eliminate step one. Maybe step three becomes interactive with
| lean4 etc. and ends in a PR with green build, but the work
| does not seem likely to end there.
|
| Put it this way: Terrence Tao is unbelievably better at maths
| than I am; Terrence Tao with lean4 is also unbelievably
| better at maths than I am with lean4. As far as the value
| embedded in all already proven mathematics, having it in
| mathlib is going to make it easy to use, but extending it in
| the way Prof. Tao can is still pretty hard.
|
| As a side note, I've extended my experimenting with GPT4 from
| writing Go and emacs lisp to asking it questions about my
| classes and it does sound smart but will happily give
| fractional results for an application of Burnside's Lemma,
| and say things like:
|
| "An example of a simple group without an element of order 2
| is any non-abelian simple group of odd order. By the Feit-
| Thompson theorem, every finite group of odd order is
| solvable, which means that non-abelian simple groups of odd
| order do not exist. However, this theorem does not rule out
| the existence of infinite simple groups of odd order."
|
| Now this answer is correct in describing how (Feit-Thompson
| theorem) to show that there are no simple groups of odd
| order, but "infinite simple groups of odd order" is pretty
| non-sensical. If the order is infinite, it is not odd.
|
| One hopes future iterations will develop understanding in a
| way that this text lacks.
| t_mann wrote:
| You don't really need understanding if you ask (or train,
| or fine-tune) the AI to produce a formalized answer, and
| then write a loop that feeds back the compiler output until
| it's correct. That doesn't guarantee that it's the answer
| that you want, but it's guaranteed to be correct, so it is
| something. You can also use this approach to produce more
| training examples, if you have time you can manually check
| and annotate whether the result is what was originally
| asked for, and then hope that the training improves the
| accuracy of the initial answer (avoiding the loaded term
| 'understanding' here). This might substantially reduce the
| amount of work that needs to be done manually after the
| first step.
|
| If I was doing a Math degree right now, that's exactly the
| kind of stuff I'd want to do for my thesis, kind of jealous
| tbh.
| zozbot234 wrote:
| There are declarative systems like Mizar and Isar that do take
| something a bit closer to natural language proof text as input.
| Outputing actual text in natural language is just an exercise
| in pretty-printing (and of course the system must know and work
| with the natural-language name for every object and statement
| you're working with, otherwise the output gets clunky).
| t_mann wrote:
| > I don't follow how the proof text is generated from lean? Or
| is it not, they are doing the verification in lean and the
| proof text is completely separate.
|
| My understanding was that the Blueprint tool that he linked is
| what's responsible for the human-readable math sections shown
| in the screenshots. I'm not saying it's easy, but it should
| definitely be doable, basically a spreadsheet like that one on
| steroids.
| alexpeattie wrote:
| The proof text is separate. Currently it's up to humans to
| ensure the proof text (written in LaTeX) properly matches the
| Lean proof.
|
| Indeed, you can see in the article that the text of Theorem 7.2
| omits for brevity details which are present in the non-pretty
| printed Lean proof (for example H is non-empty, K is a real
| number, etc.)
| InfoSecErik wrote:
| Lean has been a really exciting thing for me to watch (as an
| amateur observer), it's gonna go right up to the limits that
| Godel found.
| t_mann wrote:
| I find it almost scary how casual Terry is about all this.
| Comparing this to my own humble attempts at graduate math, I feel
| like a caveman trying to rock a basic wheelbarrow who just gets a
| visit from a guy in a helicopter. And then that guy is stretching
| out his hand 'Here, try it out, it's fun, useful and not scary at
| all'.
|
| It was always clear to me that formalization was the future of
| math ever since I heard about the four-color theorem. What I did
| not anticipate, and what Terry seems to take in stride here, was
| that we'd get an AI that can _almost_ do the job of writing the
| math as well around the same time as formalization starts to gain
| traction. The fact that I get to learn about it from the most
| friendly and humble generational genius is just the cherry on
| top.
| rq1 wrote:
| Formalism and its "derivatives" died a long time ago already.
| Even Hilbert couldn't do much about it.
|
| That being said, constructive math is still a great idea.
| t_mann wrote:
| Not sure what you mean by that - what I meant by
| formalization was to really deduce every statement in a proof
| from basic axioms and rules. So basically what Prof Tao did
| in this blog post (except that the hard rote labor has all
| been abstracted away and handed off to a machine). This kind
| of formalization is hardly dead I'd say, in fact it's just
| starting to gain traction in mainstream mathematics, as Prof
| Tao's recent work shows (if it's not too much work for a
| Fields medal winner to formalize their proofs, then what
| excuse do mere mortal mathematicians have?). So what did you
| mean?
|
| Edit: it's clear that the original four-color proof had
| nothing to do with this kind of formalization, it was just
| the debate that got me thinking about it. And tools like
| Lean4 aren't limited to constructive math afaik.
___________________________________________________________________
(page generated 2023-12-05 23:00 UTC)