I still like doing maths by pen and paper, but this is fun too.
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.
> 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 :- ))