Post #3736956

2026-07-10 20:21 UTC

1/ An experiment. Can an AI help me do my own mathematics? [1] A number of people have been advocating using AI to develop mathematics. I was accused by some peers of dismissing this, and, at the same time, attacked by other peers for even considering it as a possibility. So I took this challenge seriously, from both opposing parties, and decided to check what the latest so-called AI could contribute to something I actually care about. Thierry Coquand had already performed two experiments, getting a so-called AI to formalize two previously known facts, with previously known paper proofs. What I wanted to find out was different: whether a so-called AI can actually think about an open problem, and, at the same time, formalize its solution, or partial progress, along the way.

Replies (2)

@MartinEscardo@mathstodon.xyz 2026-07-10 20:22

2/ The open problem I chose is a 2013 conjecture, namely that the height of the dialogue tree of a System T term of type (ι⇒ι)⇒ι is below the ordinal ε₀. The results are mixed, with both progress and walls, as usual. Claude built a proof framework and an ordinal-arithmetic library from scratch, and proved the bound for a first-order fragment of the language. But the conjecture itself is still open. I do like that Claude decided on its own to consider a first-order fragment to get partial results. I didn't ask it to do that. For full disclosure, there is exactly one file in the repository I wrote by my own hand, namely [2]; everything else was written by Claude, after my prompts. [2] https://github.com/martinescardo/ClaudeExperiment/blob/master/source/MartinEscardo/README.md

Open ##3736955
@oantolin@mathstodon.xyz 2026-07-10 20:25

@MartinEscardo@mathstodon.xyz "I was accused by some peers of dismissing this, and, at the same time, attacked by other peers for even considering it as a possibility." Very common experience in recent times. 😅

Open ##4298523