Sounds like Lean 4/rocq did all the work here | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		ironbound 20 days ago \| parent \| context \| favorite \| on: Erdos 281 solved with ChatGPT 5.2 Pro Sounds like Lean 4/rocq did all the work here

wasabi991011 20 days 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.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact