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).
- Efficient Formal Verification of Bounds of Linear Programs
- JEFL: joint embedding of formal proof libraries
- Towards Knowledge Management for HOL Light
- Towards a proof of the 24-cell conjecture
- Formalizing Physics: Automation, Presentation and Foundation Issues
- Certification of Bounds of Non-linear Functions: The Templates Method
- Representing model theory in a type-theoretical logical framework
- Finding proofs in Tarskian geometry
- From Euclidean geometry to knots and nets
- Animating the Formalised Semantics of a Java-Like Language
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem
- Aligning concepts across proof assistant libraries
- Title not available (Why is that?)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- The Isabelle Framework
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
- The higher-order prover \textsc{Leo}-II
- Semi-intelligible Isar proofs from machine-generated proofs
- 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)
- 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
- On the Formalization of Cardinal Points of Optical Systems
- Formal analysis of optical systems
- TacticToe: Learning to Reason with HOL4 Tactics
- PRocH: Proof Reconstruction for HOL Light
- 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
- Random Forests for Premise Selection
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- Hierarchical invention of theorem proving strategies
- Parsing and Disambiguation of Symbolic Mathematics in the Naproche System
- Recycling proof patterns in Coq: case studies
- A Framework for Formal Reasoning about Geometrical Optics
- Effective homology of bicomplexes, formalized in Coq
- 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
- 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
- Lemmatization for Stronger Reasoning in Large Theories
- A revision of the proof of the Kepler conjecture
- The Strong Dodecahedral Conjecture and Fejes Tóth’s Conjecture on Sphere Packings with Kissing Number Twelve
- Hammer for Coq: automation for dependent type theory
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- HOL Light: An Overview
- Hammering towards QED
- Long shortest vectors in low dimensional lattices
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- Matching Concepts across HOL Libraries
- Mining State-Based Models from Proof Corpora
- Graph theory in Coq: minors, treewidth, and isomorphisms
- Formal Proofs for Nonlinear Optimization
- Formal Mathematics on Display: A Wiki for Flyspeck
- Learning to Parse on Aligned Corpora (Rough Diamond)
- Experimental mathematics, computers and the a priori
- Book Review: Dense sphere packings: a blueprint for formal proofs
- Automated Reasoning in the Wild
- Metrically homogeneous graphs of diameter 3
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
- Linear Programs for the Kepler Conjecture
- Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming
- Improving stateful premise selection with transformers
- Foreword to the special focus on formal proofs for mathematics and computer science
- 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
- 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
This page was built for software: Flyspeck
