Comment by dgellow

I feel that we don’t praise Lean enough. AFAIU it’s what enables LLMs to brute force those problems