swMATH10277MaRDI QIDQ22240FDOQ22240
Author name not available (Why is that?)
Official website: https://github.com/flyspeck/flyspeck
Source code repository: https://github.com/flyspeck/flyspeck
Cited In (only showing first 100 items - show all)
- Flyspeck II: The basic linear programs
- Formal Proofs for Nonlinear Optimization
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- JEFL: joint embedding of formal proof libraries
- Experimental mathematics, computers and the a priori
- Towards Knowledge Management for HOL Light
- Towards a proof of the 24-cell conjecture
- Representing model theory in a type-theoretical logical framework
- Finding proofs in Tarskian geometry
- From Euclidean geometry to knots and nets
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Aligning concepts across proof assistant libraries
- 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
- Matching concepts across HOL libraries
- Random forests for premise selection
- A formal proof of the Kepler conjecture
- The area method. A recapitulation
- A graph library for Isabelle
- MATHEMATICAL RIGOR AND PROOF
- Computer theorem proving in mathematics
- Busy beaver machines and the observant otter heuristic (or how to tame dreadful dragons)
- Efficient formal verification of bounds of linear programs
- Formalization of function matrix theory in HOL
- Formal analysis of continuous-time systems using Fourier transform
- The dodecahedral conjecture
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- 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
- Formal analysis of optical systems
- On contact numbers of totally separable unit sphere packings
- On Minimal Tilings with Convex Cells Each Containing a Unit Ball
- Applications of real number theorem proving in PVS
- On theorem prover-based testing
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- A learning-based fact selector for Isabelle/HOL
- Theorem proving in large formal mathematics as an emerging AI field
- Lemmatization for stronger reasoning in large theories
- Recycling proof patterns in Coq: case studies
- A Framework for Formal Reasoning about Geometrical Optics
- Effective homology of bicomplexes, formalized in Coq
- Interactive theorem proving from the perspective of Isabelle/Isar
- HOL(y)Hammer: online ATP service for HOL Light
- mizar-items
- Learning-assisted theorem proving with millions of lemmas
- Proof assistants: history, ideas and future
- Enabling high-dimensional range queries using \(k\)NN indexing techniques: approaches and empirical results
- Generating certified code from formal proofs: a case study in homological algebra
- Contact graphs of unit sphere packings revisited
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Density bounds for outer parallel domains of unit ball packings
- nFOIL
- Goeland
- MedleySolver
- Formalizing physics: automation, presentation and foundation issues
- On the formalization of cardinal points of optical systems
- The HOL Light theory of Euclidean space
- An introduction to mechanized reasoning
- Automated theorem provers: a practical tool for the working mathematician?
- Mechanically certifying formula-based Noetherian induction reasoning
- A revision of the proof of the Kepler conjecture
- Animating the formalised semantics of a Java-like language
- Certification of bounds of non-linear functions: the templates method
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- HOL Light: An Overview
- Hammering towards QED
- Long shortest vectors in low dimensional lattices
- Verified efficient enumeration of plane graphs modulo isomorphism
- The strong dodecahedral conjecture and Fejes Tóth's conjecture on sphere packings with kissing number twelve
- The Isabelle Framework
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Flyspeck I: Tame Graphs
- IMP++
- MPTP 0.2
- 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
This page was built for software: Flyspeck
