Harmonic

Today at the New York Number Theory Seminar, Wouter and Pietro were discussing their new paper. Really cool use of the AI-human feedback loop, with Aristotle as the main AI ingredient. I explained how I think formalization feels like doing the low-tech steps of algebraic geometry proofs with commutative algebra. You can have high-brow intuitions, but eventually one has to prove all the details. I wonder how this will evolve, but we are definitely at the level of assembly language being written by models like Aristotle. Tactics feel like the first glimpses of higher-level programming principles. The next step might be a more conversational style of working with the models. I am now working on a tighter integration of Lean with computer algebra languages. Stay tuned!

got a framed copy to hang by the ai team

Interesting update: a few days ago, Nathanson presented a talk at the New York Number Theory Seminar explaining how Aristotle solved some of his problems.

Interesting update: a few days ago, Nathanson presented a talk at the New York Number Theory Seminar explaining how Aristotle solved some of his problems.

I think a radical new viewpoint is emerging on the many activities that mathematicians do. Perhaps a novel profession of mathematical engineering is emerging from the early chaos of AI for mathematics. I can see very clearly that the coordination, setup, technical pursuit, and orchestration of AI systems scaled for massive mathematical efforts and projects will require a special engineering mindset that is currently lacking, or almost completely absent, in mathematical projects. The existence of such a profession is not in opposition to mathematical tinkerers who use their artisanal craft to produce genuinely novel content. As with any kind of content, someone needs to adapt it to the grand scheme of things. This is why these roles are starting to appear complementary rather than competitive. Maybe this is a temporary activity, soon to be replaced by computers, but I think the major role of mathematical engineers will be to stay in touch with the tinkerers and provide a human cushion around their internal activities. I am enjoying this kind of activity (*), where you orchestrate with models and see how the project itself becomes a challenge in design and scale. This might well mean more jobs for mathematicians. In the long run, I suspect we may become secondary cognitive powers in parts of the mathematical information chain. But I do not think this will happen very soon across the whole system. And I hope it never happens at the most human layer: the joy people feel when a new idea is born. (*) This project is essentially a lambda-calculus lab, fully integrated with classical topics such as Church’s lambda calculus, the Aristotle formal proofs system, and extensions over particular papers. I presented it to students at the workshop in Warszawa-Falenty and was very pleased with the result. I am now using this framework for proof development. What strikes me most is that this is primarily an engineering challenge: the mathematics entering the pipeline is being handled, structured, and formalized, but not radically developed inside the pipeline itself.

To my mind, what seems most important here is not so much the results themselves, nor even the particular methods used in the proof. What really matters is the workflow: the closed loop from autonomous discovery of the right constructions, to formal verification of the proof in Lean, to informalised exposition back into a manuscript that mathematicians can read, understand, rewrite, and improve. It suggests a framework in which formal proof is not merely a static final certificate, but an active part of mathematical research: a medium through which ideas are found, organised, tested, explained and made available for human judgment. That dynamic loop is the real story for me. The natural next question is how far it can be pushed.

What will mathematics look like 7 years from now? I’m really curious to hear your brief opinion.