A Lean formalization of Matiyasevič's Theorem https://arxiv.org/abs/1802.01795 ディオファントス方程式の決定不能性の証明の重要なピースであるマチャセビッチの定理のLeanによる形式化。 ディオファントス方程式の決定不能性の証明の仕方をちゃんと知らんかったので面白かった(計算機科学のすべての分野に精通できてないなw)。

証明自体は
https://github.com/leanprover/mathlib/blob/master/number_theory/dioph.lean にある。