2 ms·
Sounds like Lean 4/rocq did all the work here
by ironbound 9mo ago
Sounds like Lean 4/rocq did all the work here
- wasabi991011 9mo agoWhy do you say that? I see no mention of lean/rocq on the twitter thread, nor on the erdos problem forum thread, nor on the chatGPT conversation.