Why I’m building Plectis

As models improve, the work they produce gets bigger and harder to follow, and the tools for understanding it have to keep up. Plectis is my attempt at that, starting with mathematics.

I built it to do research I find interesting with AI, in a way where people who actually know the field can steer it. The idea is that mathematicians provide the direction: I prepare results for someone who can interpret them, their feedback changes what I work on next, and I come back with that. I’ve struggled to get that direction, so a lot of this is also me seeing how far careful preparation can get without it.

What a proof checker settles

I’m not a mathematician, and I can’t check a proof myself. I chose maths because a proof can be checked, so Lean is how I know a statement is actually proved.

Lean won’t tell you whether the statement is the one you meant, whether it was worth asking, or whether anyone can follow why it’s true. So each result comes with more than its Lean file: a short paper that sets out the argument, a long paper recording the routes that were tried, where each one stopped and how hard the nearby questions turned out to be, and seminar-style videos we’re trying to automate. Whether those explanations actually help a reader is something they still have to show. Philosophers and mathematicians wrote about exactly this in September, and the readings at the end of this page shaped how the work is set up.

What the mathematics contains

The mathematics repository¹ works on eight deliberately difficult Erdős problems. The strongest results are each checked in Lean, and most also have a Comparator check against a separately written statement. Two examples show the range.

At #257, the sum of 1/(b^a−1) over an infinite set of exponents a is irrational at every integer base b ≥ 2 whenever the reciprocals 1/a have a finite sum, and under a weaker condition the problem page states exactly. Erdős asked about every infinite set, and that question stays open.

At #1041, Lean confirms ani’s degree-seven polynomial as a counterexample to the Formal Conjectures statement of the problem. Whether that statement matches the 1958 wording still needs independent review.

The other seven questions remain open, several with partial results. The mathematics pages give each one its exact statement, papers, formal source and checking status. The papers are author-released, have not been externally peer reviewed and have no DOI. Lean checks statements; readers judge novelty and significance.

How feedback changes the work

When someone has told me what was wrong, it changed the work, and often it changed how the next piece gets made. A mathematician said one of the problem papers used names that meant nothing on a first or second reading and never said how restrictive its main hypothesis was. All sixteen problem papers were rewritten for a first-time reader, and the writing rules now require it. Another said AI-assisted mathematics rarely shows where its methods come from, so each of the eight problems got a literature review and each paper now credits its sources where it uses them.

The credit ledger² records each case and what it changed. Names stay withheld until each person says they’re happy to be named, and thanking someone there doesn’t mean they reviewed or endorsed the mathematics.

Nineteenth-century mariners contributed observations and received improved sailing charts³, so each voyage built on the last. Plectis keeps its failed routes beside its lemmas, with their conditions and limits, for the same reason: someone else, or a future model, can start from where they stopped.

Beyond mathematics

The software repository⁴ applies the same idea beyond mathematics: as AI raises what a back end can do, the front end has to rise with it, so that understanding and auditability keep up with capability. I published testable parts because I wasn’t sure about releasing the whole system. The safety doctrine sets out the rules my agents work under, my June questions ask how capability and independent scrutiny interact, and the systems and archived open-source papers explain how people can contribute direction, review, exposition, software or compute.

The name comes from plectere⁵, to weave or twist: bringing different capabilities into the same work.

Help shape the next attempt

A correction, a reference I’ve missed, a mathematical question or a better explanation can each change the work, and you don’t need to implement anything yourself. Send the specific point you think matters. With your permission I’ll record what you told me and what changed. If you prove a result, I won’t claim any priority for it and the result is yours.

Discuss a result or suggest a direction →