Fetching the paper…
Reading the bibliography…
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $\mathbb{F}^n_q$ with no three-term arithmetic progression.
Automath, a language for mathematics
N. G. de Bruijn · 1983
Earlier work this paper cites.
How to make ad-hoc polymorphism less ad hoc
P. Wadler and S. Blott · 1989
Earlier work this paper cites.
Inductively defined types
Thierry Coquand and Christine Paulin · 1990
Earlier work this paper cites.
Mizar: the first 30 years
Roman Matuszewski and Piotr Rudnicki · 2005
Earlier work this paper cites.
The four colour theorem: Engineering of a formal proof
Georges Gonthier · 2008
Earlier work this paper cites.
Point-free, set-free concrete linear algebra
Georges Gonthier · 2011
Earlier work this paper cites.
Type classes for mathematics in type theory
Bas Spitters and Eelis van der Weegen · 2011
Earlier work this paper cites.
Rank-nullity theorem in linear algebra
Jose Divasón and Jesús Aransay · 2013
Earlier work this paper cites.
The HOL Light theory of euclidean space
John Harrison · 2013
Earlier work this paper cites.
Formalization and execution of linear algebra: From theorems to algorithms
Jesús Aransay and Jose Divasón · 2014
Earlier work this paper cites.
A computer-algebra-based formal proof of the irrationality of ζ \zeta (3)
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi · 2014
Earlier work this paper cites.
The Lean theorem prover, 2014
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer · 2014
Cited alongside, same era.
Vector spaces
Holden Lee · 2014
Cited alongside, same era.
Algebraic combinatorial geometry: the polynomial method in arithmetic combinatorics, incidence combinatorics, and number theory
Terence Tao · 2014
Cited alongside, same era.
Mechanisation of AKS algorithm: Part 1 – the main theorem
Hing-Lun Chan and Michael Norrish · 2015
Cited alongside, same era.
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Sophie Bernard, Yves Bertot, Laurence Rideau, and Pierre-Yves Strub · 2016
Cited alongside, same era.
Proof pearl: Bounding least common multiples with triangles
Hing-Lun Chan and Michael Norrish · 2016
Cited alongside, same era.
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura · 2017
Later among the works it cites.
On large subsets of 𝔽 q n \mathbb{F}^{n}_{q} with no three-term arithmetic progression
Jordan S. Ellenberg and Dion Gijswijt · 2017
Later among the works it cites.
A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al · 2017
Later among the works it cites.
Homotopy type theory in Lean
Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz · 2017
Later among the works it cites.
Formalization Techniques for Asymptotic Reasoning in Classical Analysis
Reynald Affeldt, Cyril Cohen, and Damien Rouhling · 2018
Later among the works it cites.
The Lean 3 mathematical library (presentation), July 2018
Mario Carneiro · 2018
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Tests and proofs for enumerative combinatorics
Catherine Dubois, Alain Giorgetti, and Richard Genestier · 2016
Cited alongside, same era.
Polynomial methods in combinatorics
Larry Guth · 2016
Cited alongside, same era.
A symmetric formulation of the Croot-Lev-Pach-Ellenberg-Gijswijt capset bound, May 2016
Terence Tao · 2016
Cited alongside, same era.
Progression-free sets in ℤ 4 n \mathbb{Z}^{n}_{4} are exponentially small
Ernie Croot, Vsevolod F. Lev, and Péter Pál Pach · 2017
Cited alongside, same era.
A formalization of the Berlekamp-Zassenhaus factorization algorithm
Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada · 2017
Cited alongside, same era.
A motivated rendition of the Ellenberg–Gijswijt gorgeous proof that the largest subset of F 3 n F_{3}^{n} with no three-term arithmetic progression is O ( c n ) O(c^{n}) , with c = ( 5589 + 891 33 ) 3 / 8 = 2.75510461302363300022127 … c=\sqrt[3]{(5589+891\sqrt{33})}/8=2.75510461302363300022127\ldots\,
Doron Zeilberger
Cited in the paper.
Later among the works it cites.
Symmetric polynomials
Manuel Eberl · 2018
Later among the works it cites.
A corrected quantitative version of the Morse lemma
Sébastien Gouëzel and Vladimir Shchur · 2018
Later among the works it cites.
Nine chapters of analytic number theory in Isabelle/HOL
Manuel Eberl · 2019
Closest in time.
A formal proof of Hensel’s lemma over the p p -adic integers
Robert Y. Lewis · 2019
Closest in time.