I'll Still Write Formal Proofs by Myself

ChatGPT 5.2 Thinking proved the original version of a theorem about accessible elements in 6 minutes and 20 seconds; I spent 11 hours, 11 minutes, and 45 seconds to prove it.

- ChatGPT 5.2 Thinking's proof: https://paste.sr.ht/~chabulhwi/5cc4cf5c4cd6f84c20df426d5e4f4044dbf0fadb
- My proof: https://git.sr.ht/~chabulhwi/tpil-solutions/tree/ba60de58f16f4ec0400d8ba9e388984ee661d175/item/TPIL/Chapter08/Accessibility.lean#L248

I dropped out of Korea Aerospace University in 2023, and I don't know much about undergraduate mathematics, although I've been using the Lean theorem prover for four years.

I'm not sure whether I'll be able to prove undergraduate-level theorems as fast as the state-of-the-art AI agents, even after I become more knowledgeable about undergraduate mathematics.

However, I'll keep proving theorems by myself for the following reasons:

1. While trying to prove a theorem, I find out which lemmas are important for achieving my goal.
2. I understand a theorem much better after I prove it without looking at an AI agent's proof.
3. Reviewing an AI agent's proof isn't fun.

Still, it's impressive that GPT-5.3-Codex, Claude Sonnet 4.6, Claude Opus 4.6, and Gemini 3.1 Pro can write Lean 4 code to prove basic theorems about induction and recursion. Personally, I don't want to pay money for using these models, so I'll try to find ways to use them for free.