Pages that link to "Item:Q2351415"

The following pages link to Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415):

Displaying 39 items.

• MizAR 40 for Mizar 40 (Q286800) (← links)
• The higher-order prover \textsc{Leo}-II (Q287283) (← links)
• Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
• On the formal analysis of Gaussian optical systems in HOL (Q315313) (← links)
• A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
• Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
• JEFL: joint embedding of formal proof libraries (Q831932) (← links)
• Aligning concepts across proof assistant libraries (Q1640642) (← links)
• Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
• Automating formalization by statistical and semantic parsing of mathematics (Q1687711) (← links)
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574) (← links)
• HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
• TacticToe: learning to prove with tactics (Q2031416) (← links)
• Machine learning guidance for connection tableaux (Q2031418) (← links)
• Improving stateful premise selection with transformers (Q2128800) (← links)
• GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
• Finding proofs in Tarskian geometry (Q2362499) (← links)
• ENIGMA: efficient learning-based inference guiding machine (Q2364687) (← links)
• Internal Guidance for Satallax (Q2817934) (← links)
• Automated Reasoning Service for HOL Light (Q2843009) (← links)
• Random Forests for Premise Selection (Q2964471) (← links)
• Lemmatization for Stronger Reasoning in Large Theories (Q2964472) (← links)
• Formalizing Physics: Automation, Presentation and Foundation Issues (Q3453125) (← links)
• Automated Reasoning in the Wild (Q3454081) (← links)
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance (Q3541722) (← links)
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) (Q5049022) (← links)
• A FORMAL PROOF OF THE KEPLER CONJECTURE (Q5280247) (← links)
• Matching Concepts across HOL Libraries (Q5495929) (← links)
• Mining State-Based Models from Proof Corpora (Q5495930) (← links)
• Towards Knowledge Management for HOL Light (Q5495935) (← links)
• Hammering Mizar by Learning Clause Guidance (Short Paper). (Q5875448) (← links)
• Machine Learning for Inductive Theorem Proving (Q6108816) (← links)
• Machine-learned premise selection for Lean (Q6541150) (← links)
• Synergies between machine learning and reasoning -- an introduction by the Kay R. Amel group (Q6577680) (← links)
• HOL4PRS: proof recommendation system for the HOL4 theorem prover (Q6648185) (← links)
• Invariant neural architecture for learning term synthesis in instantiation proving (Q6650564) (← links)
• Graph sequence learning for premise selection (Q6650565) (← links)