Post #3736955

2026-07-10 20:22 UTC

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

Replies (2)

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

3/ Two things happened to me along the way. I still think it is more fun to work with people, in particular PhD students, than with so-called AI's. And the machine was actually OK. But just OK. Also it was impressive, e.g. writing Agda code we know we could have written ourselves, if we wanted to and if we were patient enough. Everything I discuss here is public [3], including the AI's own first-person account and every prompt I gave it. You will have to judge by yourself. I don't think I know what this means for the future, and I don't think anybody else knows either. But I am kind of sad after this experiment. [3] https://github.com/martinescardo/ClaudeExperiment

Open ##3736954
@fullyabstract@fosstodon.org 2026-07-10 21:04

@MartinEscardo@mathstodon.xyz "everything else was written by Claude ..." I'm no expert, but I believe that the concept of "written by Claude" can mean dramatically different things depending upon what it's been trained on. Suppose it was trained on a similar proof, and only had to tweak it? Are full proofs embedded in the models, so they can be extracted with the right prompts? I think the answer is yes, but again I'm no expert.

Open ##4298521