Pages that link to "Item:Q2351415"
From MaRDI portal
The following pages link to Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415):
Displaying 31 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)
- 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)
- 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)
