The Isabelle Framework

By M. Wenzel, Lawrence Charles Paulson, Tobias Nipkow. 2008

213 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Evaluation & Benchmarks

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Evaluation & Benchmarks

Citations in the corpus

Solving Quantitative Reasoning Problems with Language Models (2022, methodology): “This can be achieved using specialized programming languages that facilitate the simulation of logical and mathematical thinking using a computer, such as Coq [20], Isabelle [21], HOL4 [22], Lean [23], Metamath [24] and Mizar [25].”
Llemma: An Open Language Model For Mathematics (2023, background): “Interactive proof assistants such as Lean (de Moura et al., 2015), Isabelle (Wenzel et al., 2008), and Coq (Paulin-Mohring, 1989a;b) express mathematics in programming languages that allow for verification.”
DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models (2024, methodology): “• Formal Mathematics : We evaluate DeepSeekMath-Base using the informal-to-formal theorem proving task from (Jiang et al., 2022) on miniF2F (Zheng et al., 2021) with Isabelle (Wenzel et al., 2008) chosen to be the proof assistant.”
Autoformalization with Large Language Models (2022, methodology): “These projects relied on interactive theorem provers, such as Isabelle [48], Coq [12], HOL Light [23], and Lean [13], which are essentially programming languages that enable users to enter their statements and proofs in a formal language, and which can then be checked automatically for correctness.”
Large Language Models for Mathematical Reasoning: Progresses and Challenges (2024, background): “For example, the M INI F2F dataset (Zheng et al., 2022) stands out in ATP, featuring a series of complex Olympiad-level mathematical problems, designed to evaluate theorem-proving systems including Metamath (Yu et al., 2023), Lean (Han et al., 2022), and Isabelle (Wenzel et al., 2008).”
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, methodology): “Like Coq and HOL Light, also Isabelle [14] was used for major formalization efforts, such as the formalization of the seL4 microkernel [16].”
Premise Selection for Theorem Proving by Deep Graph Embedding (2017, unknown): “Decades of research has resulted in a variety of well-developed automated theorem provers such as Coq [12], Isabelle [13], and E [14].”
Monte Carlo Tableau Proof Search (2016, background): “2011), leanCoP (Otten 2008), and interactive theorem provers (ITPs) such as Isabelle (Wenzel et al. 2008), HOL4 (Slind and Norrish 2008), HOL Light (Harrison 1996), and Mizar (Grabowski et al.”
Monte Carlo Connection Prover (2016, background): “…Vampire (Kovács and Voronkov 2013), CVC4 (Barrett et al. 2011), leanCoP (Otten 2008), and interactive theorem provers (ITPs) such as Isabelle (Wenzel et al. 2008), HOL4 (Slind and Norrish 2008), HOL Light (Harrison 1996), and Mizar (Grabowski et al. 2010) have led to a significant…”
LLMSTEP: LLM proofstep suggestions in Lean (2023, methodology): “Interactive proof assistants such as Lean [5], Isabelle [17], and Coq [14] enable the verification of mathematics and software using specialized programming languages [2, 12].”