'A-team' of math proves a critical link between addition and sets

https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/

by digital55 • 3 years ago

274 121 3 years ago

blowski• 3 years ago

The maths goes over my head, but this paragraph was very interesting:

Tao then kicked off an effort to formalize the proof in Lean, a programming language that helps mathematicians verify theorems. In just a few weeks, that effort succeeded. Early Tuesday morning of December 5, Tao announced that Lean had proved the conjecture without any “sorrys” — the standard statement that appears when the computer can’t verify a certain step. This is the highest-profile use of such verification tools since 2021, and marks an inflection point in the ways mathematicians write proofs in terms a computer can understand. If these tools become easy enough for mathematicians to use, they might be able to substitute for the often prolonged and onerous peer review process, said Gowers.

robertlagrant• 3 years ago

If these tools become easy enough for mathematicians to use

Sick burn, Gowers.

gowld• 3 years ago

It's honest constructive criticism. Lean is very hard to use. It's even hard to install and run.

wbhart• 3 years ago

I doubt that he was intending a burn here. He's not talking about user interface issues or the like.

He's most probably, I would assume, talking about the well-known issue that formalisation tools require knowledge that a standard mathematician doesn't possess, such as the names of all the Lean tactics, how to locate the right theorem to use in mathlib (the Lean library), the necessity to write mathematics in a very formal language which is based on dependent type theory rather than based on sets (which is what most mathematicians are used to), etc.

Moreover, formalised mathematics does not work with natural language (and perhaps can't), and it will not accept informal or intuitive arguments. There are a lot of very fiddly things that have to be attended to. One can't assume that the reader is a skilled mathematicians who can easily fill in trivial details, as when writing a maths paper for expert readers.

But the Lean people are acutely aware of all of this. In my opinion he's not so much offering them much needed criticism so much as acknowledging one of the known barriers to mathematicians from outside the formalisation community getting into formalisation.

This is a major point of the article, that real, serious mathematicians have broken through that barrier recently, and it's not the first time. So things have improved enough to show that it is possible for seriously committed mathematicians to do this, even famous ones!

kmill9• 3 years ago

I helped a very little with the formalization (I filled in some trivial algebraic manipulations, and I was there for some Lean technical support).

It's exciting to see how quickly the work was done, but it's worth keeping in mind that a top mathematician leading a formalization effort is very exciting, so he could very easily scramble a team of around 20 experienced Lean users.

There aren't enough experienced Lean users to go around yet for any old project, so Gowers's point about ease of use is an important one.

Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib. It's reassuring that mathlib is being developed in such a way that new mathematics can be formalized using it. Like usual though, there was plenty missing. I think this drove a few thousand more lines of general probability theory development.

cs702• 3 years ago

I helped a very little...

Thank You for helping with the effort, even if it was only "a very little."

I love coming across comments like yours on HN.

ska• 3 years ago

Something that was necessary for the success of this was years of development that had already been

For projects like this it is often very thankless work in the beginning, and can be a real grind.

You need at least one person with a vision of how cool it will be in the (poorly defined) future, and a lot of determination.

zozbot23410• 3 years ago

Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib

Yes but the bulk of the work on this project was background as well. So the ease of use problem should be solving itself over time as more and more prereqs get filled in.

BTW, I find it interesting that mathlib is apparently also getting refactored to accommodate constructive proofs better, as part of the porting effort to Lean 4. This might encourage more CS- and program-verification minded folks to join the effort, and maybe some folks in math-foundations too (though Lean suffers there by not being able to work with the homotopy-types axioms).

rowanG077• 3 years ago

Since you seem to be an expert on this matter I have always wondered whether at some point it becomes faster to prove novel theorems using a theorem prover then doing it on paper. I imagine that quite a bit of time is wasted in proving things that are already proven. In a similar manner that if there would be no libraries, just snippets of code in papers, in computer programming a lot of time would be wasted writing the same things again. I imagine a "proof finding" tool like hoogle is a "function finding" tool could provide a lot of value here. What is your perspective on this?

westurner4• 3 years ago

so he could very easily scramble a team of around 20 experienced Lean users

What have you to say about methods such as these:

"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models" (2023) https://arxiv.org/abs/2306.15626 https://leandojo.org/

https://news.ycombinator.com/from?site=leandojo.org

( https://westurner.github.io/hnlog/#story-38435908 Ctrl-F "TheoremQA" (to find the citation and its references in my local personal knowledgebase HTML document with my comments archived in it), manually )

"TheoremQA: A Theorem-driven [STEM] Question Answering dataset" (2023) https://github.com/wenhuchen/TheoremQA#leaderboard (they check LLM accuracy with Wolfram Mathematica)

"Large language models as simulated economic agents (2022) [pdf]" https://news.ycombinator.com/item?id=34385880 :

Can any LLM do n-body gravity? What does it say when it doesn't know; doesn't have confidence in estimates?

From https://news.ycombinator.com/item?id=38354679 :

"LLMs cannot find reasoning errors, but can correct them" (2023) https://news.ycombinator.com/item?id=38353285
"Misalignment and Deception by an autonomous stock trading LLM agent" https://news.ycombinator.com/item?id=38353880#38354486

That being said, guess and check and then develop a fitting casual explanation is or is not the standard practice of science, so

https://news.ycombinator.com/item?id=38124505 https://westurner.github.io/hnlog/#comment-38124505 :

What does Mathlib have for SetTheory, ZFC, NFU, and HoTT?
Do any existing CAS systems have configurable axioms?

Does LeanDojo have configurable axioms?

From https://news.ycombinator.com/item?id=38527844 :

TIL i^4x == e^2iπx ... But SymPy says it isn't so (as the equality relation automated test assertion fails); and GeoGebra plots it as a unit circle and a line, but SymPy doesn't have a plot_complex() function to compare just one tool's output with another.

brap3• 3 years ago

Why did the verification step take so long? I imagine just verifying proofs is very efficient, no?

Or do they mean formalizing the proof in Lean is what took weeks?

adastra22• 3 years ago

They’re talking about formalizing the proof (aka writing Lean “code”).

spadufed• 3 years ago

If anybody's interested in learning more about Lean, he's been posting his experiences with the project over at @tao@mathstodon.xyz

Affric• 3 years ago

On your opening sentence against this one from the article:

feels like really one of the most basic things that we didn’t understand

Nothing can prepare us for the depth of mathematics.

westurner4• 3 years ago

If these tools become easy enough for mathematicians to use, they might be able to substitute for the often prolonged and onerous peer review process,

List of long mathematical proofs: https://en.wikipedia.org/wiki/List_of_long_mathematical_proo... :

This is a list of unusually long mathematical proofs. Such proofs often use computational proof methods and may be considered non-surveyable.
As of 2011, the longest mathematical proof, measured by number of published journal pages, is the classification of finite simple groups with well over 10000 pages. There are several proofs that would be far longer than this if the details of the computer calculations they depend on were published in full.

Non-surveyable proof: https://en.wikipedia.org/wiki/Non-surveyable_proof :

In the philosophy of mathematics, a non-surveyable proof is a mathematical proof that is considered infeasible for a human mathematician to verify and so of controversial validity.

7thaccount• 3 years ago

I wonder how much of mathematics is locked away from us as it requires a level of intelligence we may never have. Why do we assume proofs should be simple little equations or even just a few pages? Elegance? Why should the universe be so elegant? Is it because elegant structures are more efficient and use less energy?

Edit: I know some proofs like Fermat's last theorem were like dozens of pages or more, but I realize that is still within the comprehension of a well trained and gifted human being.

az226• 3 years ago

You can probably fine tune GPT4 to help mathematicians use this new tool as well.

owlbite• 3 years ago

10 years ago a crack professor unit was defunded by an academic tribunal for misconduct they didn't commit. These men promptly escaped from a maximum teaching schedule to the research underground. Today, still wanted by the activist community, they survive as proovers of fortune. If you have a problem that no one else can solve, and if you can find them, maybe you can hire The A-Team.

Agingcoder• 3 years ago

That’s funny thanks :-)

0823498723498722• 3 years ago

My favourite bit of every episode was the iconic ὅπλισις when Prof. Dr. P.H.D. Baracus first adds structure preserving maps to every object in sight then uses the snake lemma to weld them together with connecting homomorphisms. "I pity the fool who doesn't chase diagrams"

CobrastanJorji• 3 years ago

I got a little sick of the recurring joke where Prof. Dr. Baracus would complain about flat, two-dimensional, infinite surfaces, and then the team would trick him into using one anyway.

gosub100• 3 years ago

I love it when a discrete manifold comes together!

kleiba• 3 years ago

What do you think, how long until we can give conjectures to a specially trained LLM to come up with a proof?

brap3• 3 years ago

My uneducated hunch is that we’re just a few years away from “proof search” being a solved problem. But that’s only a part of mathematical research.

prmph• 3 years ago

I think you are much too optimistic.

Proof verification, though still hard to automate, seems at least tractable. I'm not a mathematician by any means, but something tells me automated proof search, in the general case, would require solving the halting problem, which means it is impossible even in principle.

waynecochran• 3 years ago

Neither RH nor P vs NP will succumb.

vakkermans• 3 years ago

Finding a proof is a search in a large space, akin to searching from abstractions to concretions. LLMs don’t do anything like this, and so you’re looking at the planning problem again. It’s not clear to me how framing this particular problem as a language problem is helpful in any case.

thisismyswamp2• 3 years ago

Playing chess & go is also search in a large tree of moves leading to particular game states

sfink• 3 years ago

Perhaps an LLM could produce a plausible-looking proof that is completely and utterly incorrect.

As a party trick.

cubefox2• 3 years ago

Language models are currently the best AI systems that solve general reasoning problems, including mathematical ones. So it seems more than obvious to model the problem of finding proofs as a language problem.

bawolff3• 3 years ago

At the same level of success as a mathematician? Never.

At the same level of success as your average high school graduate? Probably already can.

kaba02• 3 years ago

I assume an average high school graduate can solve a sudoku. LLMs are very interesting but anything “thinking”-related is not their strong suit.

auntienomen2• 3 years ago

Open conjectures are usually solved by inventing new mathematical frameworks that embed the context of the existing question. Inventing new definitions is trivial, but there's no rules that constrain the space of moves. And inventing _interesting_ new definitions is extremely hard. I wouldn't bet on LLMs doing this ever.

auntienomen2• 3 years ago

What would be nice is an LLM to aid in translation between mathematics and a theorem proving language like Lean. That might fuel a revolution in how mathematics is done.

kaba02• 3 years ago

For trivial stuff, it might be able to even now (but those can probably be solved algorithmically as well). For more complex stuff, they are not even scratching the surface, I would believe — LLMs can’t really do long, complex thoughts/inferences, which are essential for coming up with proofs, or even just to solve a sudoku (which they can’t do — no, writing a program (which was likely part of its training set) and executing that doesn’t count).

llwu• 3 years ago

I contributed a few trivial proofs to this project, and I tried enlisting GPT-4, Copilot, Moogle, and Morph Prover to help out (I did not try LLMStep or ReProver).

Out of these:

- GPT-4 answered maybe one or two questions about syntax

- Copilot autocompleted maybe 0.5%

- Moogle was helpful much more often but still often pointed to the wrong theorem in the right file; in most of those cases I could have just done go-to-def to get to the right file and scroll through it

Note that these results are actually very good! And Terence Tao seems to have a positive opinion as well. But we're very far away from automatically proving conjectures IMO.

I will say that Lean has great metaprogramming facilities to accept any type of AI innovation that might emerge. Currently I find the most helpful tactics to be `aesop?`, which is a classical search tactic that tries a bunch of substitutions and simplifications; and `exact?`, when you know there's a trivial proof but not sure of the name. But the UX for AI can be as simple as, for example, typing the `gptf` or `llmstep` tactic, and that is fully hooked into the Lean state (goals, hypotheses, etc). So there's a lot of opportunity for incremental progress in improving existing workflows (which consist of dispatching trivial manipulations with search/simplification tactics)

srcreigh• 3 years ago

It will never happen. Some open math problems are equivalent to the halting problem; and we know that finite computers can’t solve the halting problem.

MaxBarraclough• 3 years ago

That doesn't sound right, we already have automated theorem provers, as imperfect as they may be.

steego2• 3 years ago

Check out this paper:

https://leandojo.org/

People have already trained models to assist suggestion tactics. They then linked it up to ChatGPT to interactively solve proofs.

In this scenario, ChatGPT asks the model for tactic suggestions, applies it to the proof and uses the feedback from Lean to then proceed with the next step.

FYI, The programmatic interface to Lean was written by an OpenAI employee who was on the Lean team a few years ago.

Also, check out Lean’s roadmap. They aspire to position Lean to becoming a target for LLMs because it has been designed for verification from the ground up.

As math and compsci nerds contribute to mathlib, all of those proofs are also building up a huge corpus that will likely be leveraged for both verification and optimization.

If AI can make verification a lot easier, then we’re likely going to see verification change programming similarly to the way it changed electronics.

staunton2• 3 years ago

it has been designed for verification from the ground up.

It has a lot of places where you assume things work in a certain way and a lot of ways to assume it (and you can prove `false` if any of those assumptions aren't correct). I'd say it's a lot more geared towards formalizing math than verification.

There's some more things, e.g., the `Expression -> C-code` "compiler" isn't verified and neither is the C-compiler. Those could be fixed with some work (that nobody is working on currently, as far as I can tell). But the first issue seems pervasive. I don't think Lean will become a standard tool for software verification or significantly advance the discipline. Of course, I'd love to be wrong.

golly_ned• 3 years ago

Recent work on combining LLMs with theorem provers with promising initial results:

https://paperswithcode.com/paper/linc-a-neurosymbolic-approa...

Logical reasoning, i.e., deductively inferring the truth value of a conclusion from a set of premises, is an important task for artificial intelligence with wide potential impacts on science, mathematics, and society. While many prompting-based strategies have been proposed to enable Large Language Models (LLMs) to do such reasoning more effectively, they still appear unsatisfactory, often failing in subtle and unpredictable ways. In this work, we investigate the validity of instead reformulating such tasks as modular neurosymbolic programming, which we call LINC: Logical Inference via Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser, translating premises and conclusions from natural language to expressions in first-order logic. These expressions are then offloaded to an external theorem prover, which symbolically performs deductive inference. Leveraging this approach, we observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate. On ProofWriter, augmenting the comparatively small open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5 and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%, respectively. When used with GPT-4, LINC scores 26% higher than CoT on ProofWriter while performing comparatively on FOLIO. Further analysis reveals that although both methods on average succeed roughly equally often on this dataset, they exhibit distinct and complementary failure modes. We thus provide promising evidence for how logical reasoning over natural language can be tackled through jointly leveraging LLMs alongside symbolic provers. All corresponding code is publicly available at https://github.com/benlipkin/linc

cubefox2• 3 years ago

But "theorem provers" don't prove anything, they just check existing proofs for validity. That's a much less demanding task than coming up with a proof in the first place.

logtempo2• 3 years ago

Yesterday I was wondering if it's possible to have an AI that can "recreate" the mathematics as we know it, and even go further and explore unexplored paths.

Though prduced by a video explaining how AI helped to find optimization in the computation of matrix multiplication.

jmj• 3 years ago

I am working on that for my PhD!

logtempo2• 3 years ago

Ho, that's really cool! Sounds a bit like digging your own grave as mathematician but it must be very challenging

0823498723498722• 3 years ago

Unfortunately it's too late to give Theory Mine theorems named after your loved ones as gifts this year: https://www.theorymine.com/home

wslh• 3 years ago

BTW "Katalin Marton’s Lasting Legacy" [1]

[1] https://ee.stanford.edu/~gray/Kati_Marton.pdf

swayvil2• 3 years ago

You always hear "the map is not the territory". Which is to say, names are applied, models are asserted and all our fine ideas about the world are our own contrivance, not the world's.

But how close could we get?

oldandtired2• 3 years ago

Not very close at all.

Every map that is made leaves out an enormous amount of the territory because that detail is irrelevant to the map being used or created. The more detailed the map is, the more one should recognise just how much more detail is being ignored.

If you want to get close, just go to the territory itself and be there directly.

All too often, we use mathematics as a map for the actual world around and to keep that map manageable, we have to ignore much of the actual world.

swayvil2• 3 years ago

The trick would be to find a real phenomenon that expresses itself symbolically. Like discovering an animal born with a nametag.

I think you'd have to look in the realm of thought for that.

Surely it isn't just empty space where we build our memories and models. Surely it has its own landscape.

oldandtired2• 3 years ago

Now that it has been done in Lean, how about the version that can be put into Metamath?

'A-team' of math proves a critical link between addition and sets

Related Stories