Contact

It started as a private repo built for a trading system. UK financial regulation meant that seemed too hairy a path to go down without more guidance, but by then I had already built a large financial database, which I probably can’t release. This was before I had even used Claude Code.

I then discovered coding agent apps, and it all changed. I spent months and months building whatever I could come up with. I developed a doctrine for my agents, and built a frontend that would evolve with the backend to be able to see what was happening in the system.

I realised I couldn’t release the entire thing, so I abandoned what I deemed risky and focused on building a new system, Plectis, that would let me showcase cross-sections of the system.

I stopped vibe-mathing and focused on trying to build AI systems, as I realised systems can do a much better job than I could at doing the most abstract repeatable tasks, and in organising work done, and ultimately in directing and planning the efforts of AI at any given moment.

Then I picked eight Erdős problems. I didn’t expect to be able to solve them, the point was the journey getting there and what you can learn from it, so every no-go and failed route gets written down where the next person can use it.

In September a lot of mathematicians wrote about AI and mathematics, and a lot of it lands on the point I started from, that getting a result checked is not the same as understanding it. De Toffoli and Duede separate a logical proof, which Lean can certify, from an intelligible one that people can understand and build on. Henry Cohn calls unexplained AI proofs technical debt, and asks whoever pushed the button to take responsibility for the result, talk to people in the field and shed light on how it was found. Bryna Kra wants authors who can explain a proof’s mechanism and how they got there, with discovery, proof, formalisation and explanation credited separately. Daniel Litt argues that talks now show understanding better than papers do, and that working out what is interesting is the community’s job. Grant Sanderson points out that an AI proof arrives with its explanation still to be written, and no proof assistant will ever check that part. Terence Tao says the scarce thing now is a promising problem, along with knowing which nearby problems are easy, hard or out of reach. And the AGMAI recommendations of 29 September ask AI labs that release mathematics nobody yet understands to cite related work, write it up as a normal paper, formalise it as far as possible, with a Comparator challenge and a formalization.yaml, or state its formalization status if doing that would cause unacceptable delays, and say how AI was used and what it tried and failed.

So that’s basically what I’ve been trying to build as a lay person. Creating a Lean corpus is one thing, but what I think is my main contribution is the pipeline that distils it into papers that try to avoid the common pitfalls of AI-written papers, like just dropping Lean bombs: Lean for the logical part, a short paper for the intelligible part, a long paper for the routes that failed and how hard each nearby question turned out to be, and seminar-style videos we’re trying to automate, because a talk shows whether something is understood. It’s more of a proof of concept than me claiming I understand the mathematics deeply enough to explain it. If someone unknown with no understanding can get even part of the way, it’s an example of what an expert could do with the same tools. I’m not presupposing any of it is good, which is why the claims link to their evidence and why I need people who know the field to tell me what’s wrong.

Human mathematicians are meant to provide the direction. I’ve been struggling to get it, so a lot of this is me seeing how far you can get without it. Ideally a mathematician glances through, finds an idea worth their time, and either works on it themselves or emails me a direction, and we take that as the seed and get agents to attack it, given all of the failed routes and the short paper as it stands. When someone has told me what was wrong, it changed the work, and the credit ledger lists every case, with names withheld until each person says they’re happy to be named.

My biggest problem has been that nobody with expertise can really judge the entire thing, because it spans so many domains.

You will get the credit. I just want my system used.

Thank you for your time and interest.