Comment by ironbound 13 hours ago Sounds like Lean 4/rocq did all the work here 1 comment ironbound Reply wasabi991011 11 hours ago Why 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.
wasabi991011 11 hours ago Why 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.
Why 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.