3 ms·

I love Lean 4 as a general purpose programming language, but I can't use it because no current AI coding assistant can reliably work with me in Lean. I can be t

I love Lean 4 as a general purpose programming language, but I can't use it because no current AI coding assistant can reliably work with me in Lean. I can be trying six languages at once like a chess master playing an exhibition simultaneous match, and they'll all flow in Cursor using Claude 3.5 Sonnet, or even Windsurf. Then add Lean 4 and everyone chokes. On the other hand, Claude 3.5 Sonnet understands my iPad math drawings better than my colleagues. I am admittedly weird, but AI as an association engine of incomprehensible scope likes trippy. Trippy helps its reach. Philosophy never really worked until now when you can run it on a computer. AI really rewards recursive meta; it picks up speed like ice sailing. We're would-be shamans sitting around the fire a million years ago, imagining we can control the dance of the flames. With AI, we can. Claude also understands, say, computational group theory or strategies for combinatorial enumeration, remarkably well. So it can assist in math research. Formal proofs in Lean 4 may be hard to read, but the elephant in the room is how hard conventional math papers are to read. We're terrible at expressing ourselves, so reading a paper is the equivalent of reverse-engineering bad computer code to reconstruct thoughts the author failed to express. And it's embarrassing in 2025 that conventional papers can't be automatically checked. A new genre will emerge in between: In the "Centaur" model Gary Kasparov popularized after he recovered from his chess defeat by IBM's Big Blue, we want papers to actually be very careful, battle-tested prompts for AI. They will pass as conventional papers for mathematicians still trapped in amber, but they're really just prompts for both us and AI. The documentation for Lean 4 is aimed at humans. If it were designed to be a hybrid "Centaur" prompt doc, perhaps my tools would be better able to help me code in Lean 4.

Syzygies 2y ago
[flagged]
- practal 2y ago
  I am also using AI extensively to discuss my research, for example [1]. And also very excited about AITP (artificial intelligence theorem proving) [2]. [1] A Conversation with Graham Priest About Abstraction Logic. https://practal.com/press/cwgpaal/1 https://practal.com/press/cwgpaal/1 [2] Abstraction Logic Is All You Need. https://doi.org/10.5281/zenodo.14737457 https://doi.org/10.5281/zenodo.14737457
Syzygies 2y ago
Deepseek r1 is getting a lot of buzz in the last day or so. As a Chat agent in Cursor, it gets further than I've seen other AI get at writing Lean 4 code. The process is acutely painful. It can't stick to directions, and keeps trying to add proof features that it can't get to work, despite my instructions that we're using Lean 4 as a general purpose programming language. To my surprise, the code ran faster than either Haskell or Rust on a small case. There could be so many artifacts involved in such a conclusion, but larger cases blew the stack. That's just inexperienced code.

Syzygies 2y ago

[flagged]

practal 2y ago
I am also using AI extensively to discuss my research, for example [1]. And also very excited about AITP (artificial intelligence theorem proving) [2]. [1] A Conversation with Graham Priest About Abstraction Logic. https://practal.com/press/cwgpaal/1 https://practal.com/press/cwgpaal/1 [2] Abstraction Logic Is All You Need. https://doi.org/10.5281/zenodo.14737457 https://doi.org/10.5281/zenodo.14737457

Syzygies 2y ago

Deepseek r1 is getting a lot of buzz in the last day or so. As a Chat agent in Cursor, it gets further than I've seen other AI get at writing Lean 4 code. The process is acutely painful. It can't stick to directions, and keeps trying to add proof features that it can't get to work, despite my instructions that we're using Lean 4 as a general purpose programming language. To my surprise, the code ran faster than either Haskell or Rust on a small case. There could be so many artifacts involved in such a conclusion, but larger cases blew the stack. That's just inexperienced code.