Se ha publicado un artículo de razonamiento formalizado en Coq sobre SAT titulado A formalised polynomial-time reduction from 3SAT to Clique.

Sus autor es Lennard Gäher del Programming Systems Lab en la Universidad del Sarre (en inglés, Saarland University y en alemán Universität des Saarlandes) en Saarbrücken, Alemania.

Su resumen es

We present a formalisation of the well-known problems SAT and Clique from computational complexity theory. From there, a polynomial-time reduction from 3SAT, a variant of SAT where every clause has exactyly three literals, is developed and verified. All the results are constructively formalised in the proof assistant Coq, including the polynomial running time bounds. The machine model we use is the weak call-by-value lambda calculus.

El trabajo forma parte de su Bachelor’s Thesis y está dirigido por Fabian Kunze.

Se ha publicado un artículo de razonamiento formalizado sobre teoría de números titulado A formal proof of the irrationality of ζ(3).

Sus autores son

• Assia Mahboubi (del grupo Gallinette en el Inria) y
• Thomas Sibut-Pinote (del INRIA Team SpecFun y la Université Paris-Saclay)

Su resumen es

This paper presents a complete formal verification of a proof that the evaluation of the Riemann zeta function at 3 is irrational, using the Coq proof assistant. This result was first presented by Apéry in 1978, and the proof we have formalized essentially follows the path of his original presentation. The crux of this proof is to establish that some sequences satisfy a common recurrence. We formally prove this result by an a posteriori verification of calculations performed by computer algebra algorithms in a Maple session. The rest of the proof combines arithmetical ingredients and asymptotic analysis, which we conduct by extending the Mathematical Components libraries.

El código de las correspondientes teorías se encuentra aquí.