[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 :- ))