[fractorial]

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.

[lionkor]

When you say "working on" what is your actual contribution? Like, what should I imagine you do? For most people who tell AIs what to do and are proud of it, it's sadly mostly sitting around and staring at "thinking" output, and steering a bit, so I'm curious what the work looks like.

[fractorial]

Valid question. If I were further along and had the time to succinctly write up all my contributions, I would just point you at my blog post. I’m generally a poor communicator, so here goes nothing.

I designed and stood up a sovereign inference/compute on my intranet. It uses a trust model that allows for a controller (me) to spin up untrusted inference/forge machines for Lean, Sage, or other runtimes. Untrusted sandbox workers integrate directly into my custom harness as first class “attachments.” This is the “orchestration” layer. It’s mostly on open weights, by design.

I haven’t yet started SFTing since my examples corpus isn’t quite where I’d like it.

I have solved and formalized a one non-Erdos conjecture. I have formalized several pieces of another subfield that does not exist in Mathlib yet.

As for what I am currently working on, I have an idea I want to build out about how we might think about sieving algebraic structures to generating new, insightful conjectures.

Using LLMs and distributed compute in this context is just a consequence of needing tools to help visualize or materialize things that I am otherwise bad at so I could keep doing the interesting things myself.

[KajMagnus]

Interesting to read!

> contributions

One thing I think you and the other "AI math builders" have done, is to show how good the top models are at logics and reasoning.

I didn't realize how good they are, until they solved an Erdös problem. And now lots of Erdös problems!

(Plus verified that the AIs actually did solve the problems, that's not easy :- ))

[colin7snyder]

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)