Cited in
(only showing first 100 items - show all)- Graph theory in Coq: minors, treewidth, and isomorphisms
- Flyspeck II: The basic linear programs
- Formal Proofs for Nonlinear Optimization
- JEFL: joint embedding of formal proof libraries
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Experimental mathematics, computers and the a priori
- Book Review: Dense sphere packings: a blueprint for formal proofs
- Towards a proof of the 24-cell conjecture
- DRABT
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Towards Knowledge Management for HOL Light
- Representing model theory in a type-theoretical logical framework
- Finding proofs in Tarskian geometry
- From Euclidean geometry to knots and nets
- Linear Programs for the Kepler Conjecture
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Aligning concepts across proof assistant libraries
- Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- The higher-order prover \textsc{Leo}-II
- Semi-intelligible Isar proofs from machine-generated proofs
- The Isabelle Framework
- Formalization of complex analysis and matrix theory
- Improving stateful premise selection with transformers
- Foreword to the special focus on formal proofs for mathematics and computer science
- The area method. A recapitulation
- Random forests for premise selection
- Certification of real inequalities: templates and sums of squares
- Matching concepts across HOL libraries
- Towards the formalization of fractional calculus in higher-order logic
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Mining state-based models from proof corpora
- A formal proof of the Kepler conjecture
- A graph library for Isabelle
- Theorem of three circles in Coq
- Erratum to: ``Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Kähler packings and Seshadri constants on projective complex surfaces
- Flyspeck I: Tame Graphs
- Computer theorem proving in mathematics
- From informal to formal proofs in Euclidean geometry
- Internal guidance for Satallax
- Busy beaver machines and the observant otter heuristic (or how to tame dreadful dragons)
- MATHEMATICAL RIGOR AND PROOF
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Formal analysis of continuous-time systems using Fourier transform
- Formalization of function matrix theory in HOL
- Book review of: T. C. Hales, Dense sphere packings. A blueprint for formal proofs
- On exact Reznick, Hilbert-Artin and Putinar's representations
- Machine learning guidance for connection tableaux
- TacticToe: learning to prove with tactics
- Efficient formal verification of bounds of linear programs
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- The dodecahedral conjecture
- ENIGMA: efficient learning-based inference guiding machine
- The local optimality of the double lattice packing
- On the formal analysis of Gaussian optical systems in HOL
- Mathematical inference and logical inference
- Developing corpus-based translation methods between informal and formal mathematics: project description
- Equidecomposable Quadratic Regions
- Formal analysis of optical systems
- ACL2
- kcnfs
- MetiTarski
- Proviola
- IMP++
- CoqJVM
- IsaPlanner
- MPTP
- MPTP 0.2
- gensim
- MoMM
- Mizar
- Proof General
- HOL
- HOL Light
- MML
- Sledgehammer
- Clide
- ML4PG
- QMT
- MaLeCoP
- MathJax
- Polar
- MaSh
- ALF
- CakeML
- Intsolver
- NLCertify
- EAT
- Coq/SSReflect
- VSDITLU
- CERES
- gaia
- leanCoP
- SAD
- PhoX
- E Theorem Prover
- PRocH
- MaLARea
- HOLyHammer
This page was built for software: Flyspeck
