The following pages link to Flyspeck (Q22240):
Displaying 50 items.
- MizAR 40 for Mizar 40 (Q286800) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Busy beaver machines and the observant otter heuristic (or how to tame dreadful dragons) (Q306278) (← links)
- The local optimality of the double lattice packing (Q312160) (← links)
- On the formal analysis of Gaussian optical systems in HOL (Q315313) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Enabling high-dimensional range queries using \(k\)NN indexing techniques: approaches and empirical results (Q346495) (← links)
- The area method. A recapitulation (Q437042) (← links)
- Applications of real number theorem proving in PVS (Q469367) (← links)
- On theorem prover-based testing (Q470025) (← links)
- Formal analysis of optical systems (Q475384) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- Density bounds for outer parallel domains of unit ball packings (Q492221) (← links)
- An introduction to mechanized reasoning (Q504394) (← links)
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- Effective homology of bicomplexes, formalized in Coq (Q631755) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Automated theorem provers: a practical tool for the working mathematician? (Q657585) (← links)
- Computer theorem proving in mathematics (Q704001) (← links)
- Towards a proof of the 24-cell conjecture (Q722369) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- On contact numbers of totally separable unit sphere packings (Q898124) (← links)
- Generating certified code from formal proofs: a case study in homological algebra (Q968307) (← links)
- A revision of the proof of the Kepler conjecture (Q977177) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Formal analysis of continuous-time systems using Fourier transform (Q1640640) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574) (← links)
- The HOL Light theory of Euclidean space (Q1945903) (← links)
- From Kepler to Hales, and back to Hilbert (Q1946041) (← links)
- Contact graphs of unit sphere packings revisited (Q1956324) (← links)
- Long shortest vectors in low dimensional lattices (Q2005735) (← links)
- Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
- A graph library for Isabelle (Q2018659) (← links)
- On exact Reznick, Hilbert-Artin and Putinar's representations (Q2029015) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- From Euclidean geometry to knots and nets (Q2053353) (← links)
- Improving stateful premise selection with transformers (Q2128800) (← links)
- Graph theory in Coq: minors, treewidth, and isomorphisms (Q2209536) (← links)
- Lemma discovery for induction. A survey (Q2287904) (← links)
- Formalization of function matrix theory in HOL (Q2294128) (← links)
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
- Certification of real inequalities: templates and sums of squares (Q2349133) (← links)
- Theorem of three circles in Coq (Q2351412) (← links)
