Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2611.09048

LeanDojo-v2: A Comprehensive Library for AI-Assisted Theorem Proving in Lean

Ryan Hsiang·William Adkisson·Robert Joseph George·Anima Anandkumar
View original source ↗Read source document ↗Export metadata ↓

Abstract

Building on recent progress in machine learning for formal theorem proving in Lean, we introduce LeanDojo-v2: an end-to-end framework that unifies repository data extraction, LLM fine-tuning, proof search, AI autocompletion, and LLM-assisted theorem proving in a single software library. In addition, we provide Lean4Code, a lightweight IDE that integrates the various features of LeanDojo-v2 through a simple, mathematician-friendly UI. These tools will enable mathematicians and researchers to easily fine-tune language models on domain-specific Lean codebases and experiment with LLM-assisted theorem proving without a complex setup.

Explore related subjects

cs.LG

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Ryan Hsiang, William Adkisson, Robert Joseph George, Anima Anandkumar. 2026-11-06. LeanDojo-v2: A Comprehensive Library for AI-Assisted Theorem Proving in Lean. https://arxiv.org/abs/2611.09048

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Theoretical Bridge Between Long-Tailed Recognition and Continual Learning

We theoretically and empirically establish a previously unexplored connection between Long-Tailed Recognition (LTR) and Continual Learning (CL). Specifically, we show that training on a long-tailed dataset with imbalance factor $\mathrm{IF}$ drives model parameters into an $O(1/\sqrt{\mathrm{IF}})$ neighborhood of the dominant-class solution, under both uniform and exponentially decaying cardinality distributions. Building on this result, we establish an objective-level reformulation of LTR as a sequential learning problem and prove that the CL objective upper-bounds the balanced LTR loss up to a constant determined by the residual Head loss. Motivated by this connection, we introduce Continual Learning for Long-Tailed Recognition (CLTR), a principled framework that leverages standard off-the-shelf CL methods to sequentially learn Head and Tail classes while mitigating catastrophic forgetting. Extensive experiments on CIFAR100-LT, CIFAR10-LT, ImageNet-LT, and Caltech256 validate our theoretical predictions and demonstrate strong performance across diverse LTR benchmarks. In the foundation-model regime, CLTR with DualPrompt on a CLIP backbone outperforms standard adaptation baselines and is competitive with specialized methods using external semantic supervision. Our work bridges LTR and CL both theoretically and empirically, providing a principled approach for addressing long-tailed learning using standard CL strategies.

cs.LG↗
arXiv2026

Isotonic Quantile Regression Averaging for uncertainty quantification of electricity price forecasts

Quantifying the uncertainty of forecasting models is essential to assess and mitigate the risks associated with data-driven decisions, especially in volatile domains such as electricity markets. In this paper, we propose a computationally efficient isotonic variant of Quantile Regression Averaging (QRA), called Isotonic Quantile Regression Averaging (iQRA), for generating probabilistic forecasts from ensembles of point forecasts. Building on QRA, we introduce stochastic order constraints as a hyperparameter-free regularization mechanism that reduces computational complexity while maintaining competitive forecast accuracy. We further demonstrate that the same isotonic regularization principle can be applied to the smoothed estimator of QRA. In an extensive forecasting study of two European day-ahead electricity markets, we show that iQRA and its smoothed variant consistently rank among the top state-of-the-art postprocessing methods in terms of reliability and sharpness. It produces well-calibrated prediction intervals, with smoothed iQRA providing superior reliability even when compared against coverage-oriented conformal prediction. We further introduce a battery arbitrage evaluation, showing that the leading probabilistic methods achieve the highest profit per trade and that probabilistic risk control improves the economic value of trading decisions. Isotonic regularization offers a scalable hyperparameter-free variable selection for linear quantile regression, making iQRA attractive for practical decision-support systems in energy markets.

cs.LG↗
arXiv2026

Causal Representation Learning from Multimodal Clinical Records under Non-Random Modality Missingness

Clinical notes contain rich patient information, such as diagnoses or medications, making them valuable for patient representation learning. Recent advances in large language models have further improved the ability to extract meaningful representations from clinical texts. However, clinical notes are often missing. For example, in our MIMIC-IV cohort, 35.15% of patients have no eligible discharge summaries. In such cases, representations can be learned from other modalities such as structured data, chest X-rays, or radiology reports. Yet the availability of these modalities is influenced by clinical decision-making and varies across patients, potentially producing modality missing-not-at-random (MMNAR) patterns. We propose a causal representation learning framework that leverages observed data and informative missingness in multimodal clinical records. It consists of: (1) an MMNAR-aware modality fusion component that integrates structured data, imaging, and text while conditioning on missingness patterns to capture patient health and clinician-driven assignment; (2) a modality reconstruction component with latent alignment to preserve modality information in the learned representation; and (3) a multitask outcome prediction model with a rectifier that corrects for residual bias from specific modality observation patterns. Comprehensive evaluations across MIMIC-IV and eICU show consistent gains over the strongest baselines, achieving relative AUC improvements of up to 4.3% for hospital readmission and 2.7% for ICU admission.

cs.LG↗