Skip to content

ataylor24/Lean-Contextualize

BranchesTags

Repository files navigation

TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

🌐 Homepage | 🤗 Dataset | 📖 Paper

✨ News

  • 🔥 We released the datasets and evaluation code for both TaoBench and TaoBenchMathlib.

🚀 Intro

About

Lean-Contextualize builds dependency-aware Lean contexts from Jixia symbol/decl graphs. It resolves constructors, instances, and wrappers to produce the minimal context required for compiling individual problems. This is designed to enhance dataset generation from custom Lean4 codebases.

Resources

Readme
Activity

Stars

3 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

 
 
 

Contributors

Languages