The following pages link to Flyspeck (Q22240):
Displaying 50 items.
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Erratum to: ``Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)'' (Q2352503) (← links)
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
- Finding proofs in Tarskian geometry (Q2362499) (← links)
- Kähler packings and Seshadri constants on projective complex surfaces (Q2363169) (← links)
- ENIGMA: efficient learning-based inference guiding machine (Q2364687) (← links)
- Flyspeck II: The basic linear programs (Q2379683) (← links)
- Verifying integer programming results (Q2401153) (← links)
- Detecting inconsistencies in large first-order knowledge bases (Q2405258) (← links)
- Experimental mathematics, computers and the a priori (Q2441736) (← links)
- From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge (Q2663667) (← links)
- Generating candidate busy beaver machines (or how to build the zany zoo) (Q2672601) (← links)
- Book review of: T. C. Hales, Dense sphere packings. A blueprint for formal proofs (Q2795210) (← links)
- Internal Guidance for Satallax (Q2817934) (← links)
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer (Q2818017) (← links)
- Incompleteness, Undecidability and Automated Proofs (Q2829997) (← links)
- Certification of Bounds of Non-linear Functions: The Templates Method (Q2843005) (← links)
- Formal Mathematics on Display: A Wiki for Flyspeck (Q2843012) (← links)
- An Approach to the Dodecahedral Conjecture Based on Bounds for Spherical Codes (Q2848990) (← links)
- On Minimal Tilings with Convex Cells Each Containing a Unit Ball (Q2848991) (← links)
- The Strong Dodecahedral Conjecture and Fejes Tóth’s Conjecture on Sphere Packings with Kissing Number Twelve (Q2848996) (← links)
- Flyspecking Flyspeck (Q2879090) (← links)
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL (Q2914756) (← links)
- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem (Q2914757) (← links)
- Learning to Parse on Aligned Corpora (Rough Diamond) (Q2945635) (← links)
- Random Forests for Premise Selection (Q2964471) (← links)
- Lemmatization for Stronger Reasoning in Large Theories (Q2964472) (← links)
- Animating the Formalised Semantics of a Java-Like Language (Q3088008) (← links)
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism (Q3088012) (← links)
- An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time (Q3102743) (← links)
- HOL Light: An Overview (Q3183517) (← links)
- Book Review: Dense sphere packings: a blueprint for formal proofs (Q3451250) (← links)
- Formalizing Physics: Automation, Presentation and Foundation Issues (Q3453125) (← links)
- Towards the Formalization of Fractional Calculus in Higher-Order Logic (Q3453127) (← links)
- Automated Reasoning in the Wild (Q3454081) (← links)
- System Description: E.T. 0.1 (Q3454109) (← links)
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover (Q3460043) (← links)
- The Isabelle Framework (Q3543647) (← links)
- A Compiled Implementation of Normalization by Evaluation (Q3543648) (← links)
- The dodecahedral conjecture (Q3584349) (← links)
- Flyspeck I: Tame Graphs (Q3613398) (← links)
- MATHEMATICAL INFERENCE AND LOGICAL INFERENCE (Q4557165) (← links)
- Computational logic: its origins and applications (Q4559535) (← links)
- Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming (Q4611311) (← links)
- TacticToe: Learning to Reason with HOL4 Tactics (Q4645730) (← links)
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
- PRocH: Proof Reconstruction for HOL Light (Q4928443) (← links)
- Metrically homogeneous graphs of diameter 3 (Q4991900) (← links)
