Flyspeck
From MaRDI portal
Software:22240
swMATH10277MaRDI QIDQ22240FDOQ22240
Author name not available (Why is that?)
Source code repository: https://github.com/flyspeck/flyspeck
Cited In (only showing first 100 items - show all)
- Flyspeck II: The basic linear programs
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- JEFL: joint embedding of formal proof libraries
- 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 Isabelle Framework
- 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
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- The area method. A recapitulation
- Flyspeck I: Tame Graphs
- A graph library for Isabelle
- 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
- 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
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- Hierarchical invention of theorem proving strategies
- 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
- Learning-assisted theorem proving with millions of lemmas
- 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
- A Compiled Implementation of Normalization by Evaluation
- 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
- Hammer for Coq: automation for dependent type theory
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- PRocH: proof reconstruction for HOL Light
- HOL Light: An Overview
- Proof pearl: a probabilistic proof for the girth-chromatic number theorem
- Parsing and disambiguation of symbolic mathematics in the Naproche system
- Hammering towards QED
- Long shortest vectors in low dimensional lattices
- Verified efficient enumeration of plane graphs modulo isomorphism
- TacticToe: learning to reason with HOL4 tactics
- The strong dodecahedral conjecture and Fejes Tóth's conjecture on sphere packings with kissing number twelve
- Graph theory in Coq: minors, treewidth, and isomorphisms
- Formal Proofs for Nonlinear Optimization
- Experimental mathematics, computers and the a priori
- Book Review: Dense sphere packings: a blueprint for formal proofs
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Linear Programs for the Kepler Conjecture
- Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming
- 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
- Mining state-based models from proof corpora
- Towards the formalization of fractional calculus in higher-order logic
- Certification of real inequalities: templates and sums of squares
- 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
- From informal to formal proofs in Euclidean geometry
- MATHEMATICAL RIGOR AND PROOF
- Internal guidance for Satallax
- Title not available (Why is that?)
- Formalization of function matrix theory in HOL
- Formal analysis of continuous-time systems using Fourier transform
- 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
- Developing corpus-based translation methods between informal and formal mathematics: project description
- Mathematical inference and logical inference
This page was built for software: Flyspeck
