Rendered at 04:26:20 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
vessenes 3 hours ago [-]
Very interesting, on many levels: first, the raw additional compute / search harness is worth reading about; huge numbers of Lean 4 theorems, thousands of vCPUs available for spreading out search, embedding databases of proofs, all very interesting.
Second, the proofs -- I understand the Lean 4 proofs to be refereed by Fable, and generated by Chat 5.6 Sol. Unlike the leaked proof of the Cycle Double Cover Conjecture last week which had a very nicely readable nearly humanlike writeup, the proof summaries (from Fable) read like Claude tends to read to me these days - real difficulty with the theory of mind of the reader, they are filled with technical phrases, acknowledgment of hard bits and oblique reference to solutions. In short, they suck. I didn't see the word load-bearing, but I bet it's there.
That said, a Lean 4 proof is a pretty compelling output artifact. I find it interesting that it's an additional type of effort to turn these into human readable / appreciable / beautiful / non-shitty proofs.
To those who say who cares -- indeed. But. One of the major reasons things like the Erdos problems are valuable is that they can at times spur new techniques and concepts. The best of these concepts are applied elsewhere, advancing the frontier. While we gain a lot from solving these problems, we'll gain even more from that next step of distillation / explanation into something humans and computers can grok together. I'd hope that with so many tentatively marked 'solved' we will see some new techniques / ontology / concepts. If not, still pretty amazing.
colin7snyder 35 minutes ago [-]
This is great feedback (thank you for taking the time), & you especially bring up a fair point on the writeups needing to be more human readable. I'll work on that
3 hours ago [-]
fractorial 2 hours ago [-]
My mouth is agape at the fact that this project
is basically what I have been working on non-stop
for the last three weeks and just yesterday gotten
to the point of evaluating; hats off... I only have
one novel proof (non-Erdos) and 13 first-time
formalizations thus far.
I still like doing maths by pen and paper, but
this is fun too.
colin7snyder 30 minutes ago [-]
Thank you for the kind words! I agree, it's exciting that we can now build advanced AI systems for solving novel math (but i still love pen & paper too)
crawfordcomeaux 1 hours ago [-]
[dead]
orlandpm 3 hours ago [-]
Who is funding this? Sounds like a fun experiment but that’s a huge amount of compute if I understand correctly.
Choco31415 2 hours ago [-]
According to a quick google search:
"He is currently CTO at Xinobi AI, a Japan-based startup developing personal AI agents."
colin7snyder 37 minutes ago [-]
This is a self funded weekend project for me. It's not associated with any employer (:
orlandpm 26 minutes ago [-]
> dedicated 60-vCPU server
How many of these are you paying for out of pocket??
zitterbewegung 1 hours ago [-]
I was studying Erdos problems by only taking ChatGPT 5.5 outputs and just asking it to keep on attempting to solve it by asking it to go further. I haven't started doing this with chatgpt 5.6 I have some partial results here https://chatgpt.com/g/g-p-69f03400f420819192418b18ca90ffee-d...
What was really interesting is that during the process it was able to find lemmas or theorems that might be related or relevant to be published.
While I was doing that I was also trying to use Aristotle to do the Lean formalization and I have a WIP system to do that at https://github.com/aconsapart/thesisus/
ralusek 6 minutes ago [-]
I didn't know people could just have GPT running on their own hardware. How does one...do that? Do you have a special relationship with OpenAI and they lock down your servers or something?
gravypod 3 hours ago [-]
What kind of harness does the exploration? Where did the corpus of Lean proofs come from? Is the code backing Ton 618 open source?
matteoraso 3 hours ago [-]
I've been wanting to experiment with using AI to prove math theorems, but compute is obviously a massive limiting factor here. Are there any plans to open source this?
esafak 2 hours ago [-]
Isn't this sucking the fun out of math? It's not like we're going to get any tangible benefit out of them, so why not let mathematicians keep their jobs?
zamadatix 1 hours ago [-]
The thing about math is we don't usually know what is pure fancy and what is civilization altering until far after the discovery. Once in a while it's a real targeted crack at something practical but most often it's collecting things which seem trial until you use them together and suddenly you have computers running LLMs.
If it were really just about funding people who like math to have fun then it's easy to do forever: just don't have them look at the results and keep paying.
esafak 1 hours ago [-]
What is their pay going to be justified by once computers start conjecturing and proving theorems on their own?
ralusek 7 minutes ago [-]
This is kind of insane reasoning. It's basically asking "what is their pay going to be justified by once their pay isn't justified?"
derektank 58 minutes ago [-]
Attending department faculty meetings
Reubend 1 hours ago [-]
Isn't the pursuit of knowledge alone good enough?
Legend2440 52 minutes ago [-]
The job of a mathematician is to study mathematics, not to create proofs.
An automatic proof solver doesn't make mathematicians obsolete any more than the excel sheet made accountants obsolete.
1 hours ago [-]
yieldcrv 2 hours ago [-]
or get those bright minds out of academia daycare and back to more actionable needs such as steering agents
no_multitudes 2 hours ago [-]
This will keep happening until we stop people from doing it.
Second, the proofs -- I understand the Lean 4 proofs to be refereed by Fable, and generated by Chat 5.6 Sol. Unlike the leaked proof of the Cycle Double Cover Conjecture last week which had a very nicely readable nearly humanlike writeup, the proof summaries (from Fable) read like Claude tends to read to me these days - real difficulty with the theory of mind of the reader, they are filled with technical phrases, acknowledgment of hard bits and oblique reference to solutions. In short, they suck. I didn't see the word load-bearing, but I bet it's there.
That said, a Lean 4 proof is a pretty compelling output artifact. I find it interesting that it's an additional type of effort to turn these into human readable / appreciable / beautiful / non-shitty proofs.
To those who say who cares -- indeed. But. One of the major reasons things like the Erdos problems are valuable is that they can at times spur new techniques and concepts. The best of these concepts are applied elsewhere, advancing the frontier. While we gain a lot from solving these problems, we'll gain even more from that next step of distillation / explanation into something humans and computers can grok together. I'd hope that with so many tentatively marked 'solved' we will see some new techniques / ontology / concepts. If not, still pretty amazing.
I still like doing maths by pen and paper, but this is fun too.
"He is currently CTO at Xinobi AI, a Japan-based startup developing personal AI agents."
How many of these are you paying for out of pocket??
What was really interesting is that during the process it was able to find lemmas or theorems that might be related or relevant to be published.
While I was doing that I was also trying to use Aristotle to do the Lean formalization and I have a WIP system to do that at https://github.com/aconsapart/thesisus/
If it were really just about funding people who like math to have fun then it's easy to do forever: just don't have them look at the results and keep paying.
An automatic proof solver doesn't make mathematicians obsolete any more than the excel sheet made accountants obsolete.