2 citations · 3 across the 2 of their papers we have counts for
Showing math.LOShow all
2 papers · 1 filter
math.LO2018
A Lean formalization of Matiyasevič's Theorem
Mario Carneiro
In this paper, we present a formalization of Matiyasevič's theorem, which states that the power function is Diophantine, forming the last and hardest piece of the MRDP theorem of t…
math.LO2015★ 1 cited
GCH implies AC, a Metamath Formalization
Mario Carneiro
We present the formalization of Specker's "local" version of the claim that the Generalized Continuum Hypothesis implies the Axiom of Choice, with particular attention to some extr…