Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash、Adam Topazは、Kevin Buzzardのブログで「How to Formalize All of Mathematics」と題されたブログ記事を執筆しました。これは、数学文献全体を自動的に形式化するという最近の提案に関するものです。形式数学に関する問題は、非形式的なものに関する問題と並行しています[...]