Flyspeck

No author found.

Source code repository: https://github.com/flyspeck/flyspeck

Related Items (only showing first 100 items - show all)

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 ⋮ Improving stateful premise selection with transformers ⋮ MizAR 40 for Mizar 40 ⋮ The higher-order prover \textsc{Leo}-II ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ JEFL: joint embedding of formal proof libraries ⋮ Book Review: Dense sphere packings: a blueprint for formal proofs ⋮ Busy beaver machines and the observant otter heuristic (or how to tame dreadful dragons) ⋮ From informal to formal proofs in Euclidean geometry ⋮ Formalizing Physics: Automation, Presentation and Foundation Issues ⋮ Towards the Formalization of Fractional Calculus in Higher-Order Logic ⋮ Automated Reasoning in the Wild ⋮ System Description: E.T. 0.1 ⋮ The local optimality of the double lattice packing ⋮ Flyspeck II: The basic linear programs ⋮ On the formal analysis of Gaussian optical systems in HOL ⋮ Formal analysis of continuous-time systems using Fourier transform ⋮ Aligning concepts across proof assistant libraries ⋮ FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover ⋮ HOL Light: An Overview ⋮ Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL ⋮ Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem ⋮ A learning-based fact selector for Isabelle/HOL ⋮ MATHEMATICAL INFERENCE AND LOGICAL INFERENCE ⋮ Computational logic: its origins and applications ⋮ Enabling high-dimensional range queries using \(k\)NN indexing techniques: approaches and empirical results ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ Hammer for Coq: automation for dependent type theory ⋮ Verifying integer programming results ⋮ Detecting inconsistencies in large first-order knowledge bases ⋮ Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge ⋮ Learning to Parse on Aligned Corpora (Rough Diamond) ⋮ Generating candidate busy beaver machines (or how to build the zany zoo) ⋮ On contact numbers of totally separable unit sphere packings ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ Random Forests for Premise Selection ⋮ Lemmatization for Stronger Reasoning in Large Theories ⋮ Effective homology of bicomplexes, formalized in Coq ⋮ The HOL Light theory of Euclidean space ⋮ From Kepler to Hales, and back to Hilbert ⋮ The area method. A recapitulation ⋮ Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming ⋮ Graph theory in Coq: minors, treewidth, and isomorphisms ⋮ Contact graphs of unit sphere packings revisited ⋮ Experimental mathematics, computers and the a priori ⋮ Representing model theory in a type-theoretical logical framework ⋮ Applications of real number theorem proving in PVS ⋮ On theorem prover-based testing ⋮ Automated theorem provers: a practical tool for the working mathematician? ⋮ The Isabelle Framework ⋮ A Compiled Implementation of Normalization by Evaluation ⋮ Formal analysis of optical systems ⋮ Recycling proof patterns in Coq: case studies ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Density bounds for outer parallel domains of unit ball packings ⋮ An introduction to mechanized reasoning ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ TacticToe: Learning to Reason with HOL4 Tactics ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Long shortest vectors in low dimensional lattices ⋮ Generating certified code from formal proofs: a case study in homological algebra ⋮ The dodecahedral conjecture ⋮ PRocH: Proof Reconstruction for HOL Light ⋮ Computer theorem proving in mathematics ⋮ A revision of the proof of the Kepler conjecture ⋮ 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 ⋮ Towards a proof of the 24-cell conjecture ⋮ On exact Reznick, Hilbert-Artin and Putinar's representations ⋮ TacticToe: learning to prove with tactics ⋮ Machine learning guidance for connection tableaux ⋮ Thomas Hales. Dense Sphere Packings: A Blueprint for Formal Proofs. Cambridge University Press, Cambridge, 2012, xiv + 271 pp. ⋮ Flyspeck I: Tame Graphs ⋮ Lemma discovery for induction. A survey ⋮ Formalization of function matrix theory in HOL ⋮ From Euclidean geometry to knots and nets ⋮ Internal Guidance for Satallax ⋮ Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer ⋮ Animating the Formalised Semantics of a Java-Like Language ⋮ Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ Incompleteness, Undecidability and Automated Proofs ⋮ An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time ⋮ Metrically homogeneous graphs of diameter 3 ⋮ Proof assistants: history, ideas and future ⋮ Certification of Bounds of Non-linear Functions: The Templates Method ⋮ Formal Mathematics on Display: A Wiki for Flyspeck ⋮ An Approach to the Dodecahedral Conjecture Based on Bounds for Spherical Codes ⋮ On Minimal Tilings with Convex Cells Each Containing a Unit Ball ⋮ The Strong Dodecahedral Conjecture and Fejes Tóth’s Conjecture on Sphere Packings with Kissing Number Twelve ⋮ Certification of real inequalities: templates and sums of squares ⋮ 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 ⋮ Flyspecking Flyspeck

This page was built for software: Flyspeck