scientific article; zbMATH DE number 7649964

DOI10.4230/LIPICS.ITP.2019.15MaRDI QIDQ5875423zbMATH OpenFDO

Authors Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis

Publication date 3 February 2023

Full work available at URL https://arxiv.org/abs/1907.01449

zbMATH Keywords

cap set problemcombinatoricsformal prooflean

Mathematics Subject Classification ID

Cites work

• A corrected quantitative version of the Morse lemma
• A formal proof of the Kepler conjecture
• Algebraic combinatorial geometry: the polynomial method in arithmetic combinatorics, incidence combinatorics, and number theory
• Formalization and execution of linear algebra: from theorems to algorithms
• Homotopy type theory in Lean
• scientific article; zbMATH DE number 6603592 (Why is no real title available?)
• The HOL Light theory of Euclidean space
• Type classes for mathematics in type theory

Cited in

(4)

• What is the point of computers? A question for pure mathematicians
• Formalising the Kruskal-Katona theorem in Lean
• Formalizing the Solution to the Cap Set Problem
• Mathematical reasoning and the computer

Describes a project that uses

Uses Software

• kepler98
• Archive of Formal Proofs

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875423)