A FORMAL PROOF OF THE KEPLER CONJECTURE

A Learning-Based Fact Selector for Isabelle/HOL

scientific article

A Survey of Languages for Formalizing Mathematics

scientific article

A study of continuous vector representations for theorem proving

scientific article

Algebraic Analysis of Huzita’s Origami Operations and Their Extensions

scientific article

Aligning concepts across proof assistant libraries

scientific article

Automated Reasoning Service for HOL Light

scientific article

Automating Formalization by Statistical and Semantic Parsing of Mathematics

scientific article

Automating Side Conditions in Formalized Partial Functions

CTP-based programming languages?

Certification of Nonclausal Connection Tableaux Proofs

scientific article

Certified Computer Algebra on Top of an Interactive Theorem Prover

Certified Connection Tableaux Proofs for HOL Light and TPTP

scientific article

Classification of Alignments Between Concepts of Formal Mathematical Systems

Communicating Formal Proofs: The Case of Flyspeck

Concrete Semantics with Coq and CoqHammer

scientific article

Cooperative Repositories for Formal Proofs

Counting Derangements, Non Bijective Functions and the Birthday Problem

Deep Network Guided Proof Search

scientific article

Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description

scientific article

Efficient Low-Level Connection Tableaux

scientific article

Exploration of neural machine translation in autoformalization of mathematics in Mizar

scientific article

FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover

scientific article

First Experiments with Neural Translation of Informal to Formal Mathematics

scientific article

Formal Mathematics on Display: A Wiki for Flyspeck

Formal microeconomic foundations and the first welfare theorem

scientific article

Formalizing Physics: Automation, Presentation and Foundation Issues

scientific article

GRUNGE: A Grand Unified ATP Challenge

scientific article

General Bindings and Alpha-Equivalence in Nominal Isabelle

General Bindings and Alpha-Equivalence in Nominal Isabelle

Goal Translation for a Hammer for Coq (Extended Abstract)

scientific article

HOL(y)Hammer: Online ATP Service for HOL Light

Hammer for Coq: Automation for Dependent Type Theory

scientific article published on 27 February 2018

Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems

scientific article

Isabelle Formalization of Set Theoretic Structures and Set Comprehensions

scientific article

Isabelle Import Infrastructure for the Mizar Mathematical Library

scientific article

JEFL: Joint Embedding of Formal Proof Libraries

scientific article

Learning to Parse on Aligned Corpora (Rough Diamond)

scientific article

Learning-Assisted Automated Reasoning with Flyspeck

Learning-assisted theorem proving with millions of lemmas.

scientific article published in July 2015

Lemma Mining over HOL Light

Lemmatization for Stronger Reasoning in Large Theories

scientific article

MaSh: Machine Learning for Sledgehammer

scholarly article by Daniel Kühlwein et al published 2013 in Lecture Notes in Computer Science

Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq

scientific article

Machine Learning Guidance for Connection Tableaux

scientific article

Machine Learning of Coq Proof Guidance: First Experiments

scientific article

Matching Concepts across HOL Libraries

scientific article

Merging Procedural and Declarative Proof

Metis-based Paramodulation Tactic for HOL Light

scientific article

MizAR 40 for Mizar 40

Monte Carlo Tableau Proof Search

scientific article

PRocH: Proof Reconstruction for HOL Light

Premise Selection and External Provers for HOL4

scientific article

Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic

scientific article

Proceedings 10th International Workshop On User Interfaces for Theorem Provers

Progress in the Independent Certification of Mizar Mathematical Library in Isabelle

scientific article

Proof Assistant Decision Procedures for Formalizing Origami

Property Preserving Embedding of First-order Logic

scientific article

Quotients revisited for Isabelle/HOL

Random Forests for Premise Selection

scientific article

Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem

Relaxed Weighted Path Order in Theorem Proving

scientific article

SIE – Intelligent Web Proxy Framework

Scalable LCF-Style Proof Translation

Semantics of Mizar as an Isabelle Object Logic

scientific article

Sharing HOL4 and HOL Light Proof Knowledge

scientific article

System Description: E.T. 0.1

scientific article

TacticToe: Learning to Prove with Tactics

scientific article

TacticToe: Learning to Reason with HOL4 Tactics

scientific article

Towards Formal Foundations for Game Theory

scientific article

Towards Formal Proof Metrics

scientific article

Towards Knowledge Management for HOL Light

scientific article

Towards a Mizar environment for Isabelle: foundations and language

scientific article

Towards a Unified Ordering for Superposition-Based Automated Reasoning

scientific article

Web Interfaces for Proof Assistants

Wikis and Collaborative Systems for Large Formal Mathematics

scientific article