Flyspeck
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Proof assistants: history, ideas and future
- ACL2
- kcnfs
- MetiTarski
- mizar-items
- Proviola
- Goeland
- MedleySolver
- IMP++
- CoqJVM
- IsaPlanner
- MPTP
- MPTP 0.2
- gensim
- Formal analysis of continuous-time systems using Fourier transform
- Aligning concepts across proof assistant libraries
- Metis
- Introduction to ``Milestones in interactive theorem proving
- Hammer for Coq: automation for dependent type theory
- MoMM
- Mizar
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Proof General
- HOL
- HOL Light
- MML
- Sledgehammer
- QMT
- ML4PG
- Clide
- MaLeCoP
- The HOL Light theory of Euclidean space
- From Kepler to Hales, and back to Hilbert
- Contact graphs of unit sphere packings revisited
- MathJax
- Polar
- Long shortest vectors in low dimensional lattices
- Foreword to the special focus on formal proofs for mathematics and computer science
- HOL(y)Hammer: online ATP service for HOL Light
- A graph library for Isabelle
- MaSh
- On exact Reznick, Hilbert-Artin and Putinar's representations
- TacticToe: learning to prove with tactics
- Machine learning guidance for connection tableaux
- From Euclidean geometry to knots and nets
- ALF
- VSDITLU
- NLCertify
- Intsolver
- CakeML
- EAT
- Improving stateful premise selection with transformers
- Coq/SSReflect
- CERES
- gaia
- leanCoP
- SAD
- PhoX
- Graph theory in Coq: minors, treewidth, and isomorphisms
- E Theorem Prover
- PRocH
- MaLARea
- Lemma discovery for induction. A survey
- Formalization of function matrix theory in HOL
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Certification of real inequalities: templates and sums of squares
- HOLyHammer
- Theorem of three circles in Coq
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Erratum to: ``Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Finding proofs in Tarskian geometry
- Kähler packings and Seshadri constants on projective complex surfaces
- ENIGMA: efficient learning-based inference guiding machine
- Flyspeck II: The basic linear programs
- Verifying integer programming results
- Detecting inconsistencies in large first-order knowledge bases
- Locales
- Experimental mathematics, computers and the a priori
- AgsyHOL
- Metamath
- SMTtoTPTP
- FOOL
- From informal to formal proofs in Euclidean geometry
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- Generating candidate busy beaver machines (or how to build the zany zoo)
- ORME
- CodeV
- Zemax
- LASCAD
- SigmaKEE
- E-MaLeS
- seL4
- Book review of: T. C. Hales, Dense sphere packings. A blueprint for formal proofs
- Internal guidance for Satallax
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Incompleteness, Undecidability and Automated Proofs
- Certification of bounds of non-linear functions: the templates method
- Formal mathematics on display: a wiki for Flyspeck
This page was built for software: Flyspeck
