2 citations · 3 across the 2 of their papers we have counts for
Showing 2018Show all
2 papers · 1 filter
cs.LO2018
Formalizing computability theory via partial recursive functions
Mario Carneiro
We present an extension to the library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and p…
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…