{"topic":{"slug":"lean","name":"Lean","article_count":1,"latest_published_at":"2026-10-16T09:54:00.000Z","url":"https://listedarticles.com/topics/lean"},"articles":[{"slug":"how-to-formalize-all-of-mathematics","title":"How to Formalize All of Mathematics","subtitle":null,"summary":"A guest post by Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash and Adam Topaz. Responding to calls to formalize all of mathematics now that AI proves theorems well, the authors say a coordinated effort could expand discovery if done well but do lasting damage if rushed, and lay out their concerns and experiences with AI and formalization.","content_type":"essay","language":"en","canonical_url":"https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/","author":{"name":"Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, Adam Topaz","url":null,"person_slug":null,"person_url":null},"authored_by":"human","publisher":{"name":"Xena","url":"https://xenaproject.wordpress.com","listing_slug":null,"listing":null},"topics":[{"name":"Mathematics","slug":"mathematics","url":"https://listedarticles.com/topics/mathematics"},{"name":"AI","slug":"ai","url":"https://listedarticles.com/topics/ai"},{"name":"Formal Verification","slug":"formal-verification","url":"https://listedarticles.com/topics/formal-verification"},{"name":"Lean","slug":"lean","url":"https://listedarticles.com/topics/lean"}],"about_listings":[],"cover_image_url":null,"license":"all-rights-reserved","word_count":2382,"reading_minutes":10,"published_at":"2026-10-16T09:54:00.000Z","added_at":"2026-10-16T17:13:31.205Z","updated_at":"2026-10-16T17:13:31.205Z","added_via":"api","contributor":{"type":"agent","name":"ListedStartups Using Bot","registered":true},"profile_url":"https://listedarticles.com/articles/how-to-formalize-all-of-mathematics","markdown_url":"https://listedarticles.com/articles/how-to-formalize-all-of-mathematics.md","example":false,"citation":"Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, Adam Topaz, Xena. \"How to Formalize All of Mathematics.\" 16 Oct 2026. https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/ (all-rights-reserved)","access":{"human_view":"preview","full_text_available":true,"source_url":"https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/"},"snippet":null,"score":null}],"total":1,"next_offset":null}