ORGANIZATION · ORIGINATING FUNDER
XTX Markets
A cross-source view of this organization’s disclosed roles, grants, and current evaluator evidence. Totals include only published row-level amounts.
$0 in published row amounts · 0 missing amounts
$0 in published row amounts · 0 missing amounts
$0 in published row amounts · 28 missing amounts
ORIGINATED GRANTS
Where funding flowed.
Showing the newest 24 of 28 current source records. Known row amounts total $0.
Bridging Proof and Computation
The project focuses on developing an extensible, native interface between Lean and the computational algebra system (CAS) Macaulay2 (M2) to enhance the integration between…
Leaning and Rocq'ing
This project harnesses the power of large language models (LLMs) to facilitate translation of statements and proofs between different interactive theorem provers (ITPs), such…
A Dataset of Modern Formalized Theorem Statements
This project creates a public dataset of hundreds of formalized statements of recent theorems from top journals, such as the Annals of Mathematics. In…
An AI-Focused Tactic for Language Learning
The project aims to enhance AI proof agents by developing a domain-specific tactic language for Lean, designed to better align with AI capabilities and…
Bridging AI, Proof Assistants, and Mathematical Data (BRIDGE)
The BRIDGE project aims to integrate AI with proof assistants and mathematical data by creating and curating large-scale datasets and dependency graphs from formalized…
LeanTutor
LeanTutor revisits the way undergraduate students learn mathematical proving with the help of interactive theorem provers (ITPs) and large language models (LLMs). LeanTutor aims…
Copilots for Isabelle
Isabelle is one of the most popular proof assistants which has hosted landmark verification results in both mathematics and computer science. As a team…
Polymath Plus
Polymath Plus is a next-generation online collaboration platform that integrates large-scale human participation with AI-based reasoning to advance mathematical discovery. Building on the original…
Databases of Structured Motivated Proofs
The project aims to significantly enhance AI-driven mathematical research by developing a comprehensive database of motivated proofs, where each idea's origin is clearly documented.…
GNN-SMT
Stanford Centaur Lab takes a two-pronged approach to proof automation in Lean 4: Lean-SMT and a general theorem proving agent. Lean-SMT integrates SMT (Satisfiability…
A Structured Representation of Tactics for Machine-Assisted Theorem Proving
This project develops a machine learning-driven approach to creating tactics for interactive theorem proving. The project will represent tactics as algebraic objects in a…
Document-Level Autoformalization
The project will develop open-source tools to automate the formalization of mathematical documents, enabling algorithmic verification of research-level mathematics using the Lean proof assistant.…
Bridging Complexity and Automation to Advance Automatic Theorem Proving
This project automated theorem proving through three innovative research directions that address key conceptual questions about proof difficulty, tractability and performance scaling. In particular,…
New Categorical and Topological Foundations For AI and Machine Learning
The project explores novel neural network architectures based on more bespoke mathematical representation spaces and structures, including sheaf theory and category theory. These novel…
Game Over or QED?
The Lean Game Server project aims to broaden the reach and impact of computer-assisted theorem proving by providing an accessible introduction to mathematical formalization…
LeanAide
Purpose not published.
Mathbench
The MathBench project aims to advance the evaluation of AI models in mathematical reasoning by introducing a novel dataset of annotated proofs. This dataset…
Learning to do Math with Vampires and Spiders
This project aims to enhance the capabilities of the fully automated theorem prover, Vampire, by integrating specific mathematical constructs such as infinite series and…
Large Language Models for Lattice-Theoretic Reasoning of Reactive Programs
The project aims to advance AI for mathematical reasoning by developing a novel approach to proving refinement laws using a Large Language Model (LLM)…
Vellum
The Vellum project builds an open-source framework, where large language models (LLMs) act as planners and interface with multiple interactive theorem-provers (ITPs) and automated…
Crowdsourcing and Reinventing the Next Generation of Dynamic and Scalable Math Benchmarks
The project seeks to create a community-driven platform that can produce, validate and iterate on benchmark mathematical problems at scale, with a view of…
Constraining LLMs for Theorem Proving
The goal of this project is to advance autoformalization—the task of translating informal mathematics into formal statements that can be automatically checked by state-of-the-art…
Sketchpad
Sketchpad is an AI-powered system for converting natural language proofs into structured formal sketches, designed to assist formal mathematics practitioners working in both Isabelle…
DEEPER
The "DEEPER" project aims to revolutionize automated theorem proving by integrating advanced machine learning techniques as guides to state-of-the-art automatic theorem provers (ATPs). By…