sean-lamont/bait

Official repository for the AAAI 2024 paper BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving.

Standard ML

253 commits

updated Oct 10, 2025

sean-lamont.github.io/bait

See the code

README

BAIT: Benchmarking Architectures for Interactive Theorem-Proving

BAIT is a platform for accelerating research in the application of AI to Interactive Theorem-Proving (AI-ITP). Please see the website for the complete documentation and more information.

artificial-intelligence

benchmark-framework

machine-learning

theorem-proving

Contributors

sean-lamont

253 commits

Similar repos

ericjiang18/Awesome-Formal-Mathematics

Xinze-Li-Moqian/awesome-ai4math

The ecosystem reshaping mathematics.

kaiyuy/ASTactic

Model

The ASTactic model in the paper:

drzo/ASTactic

bytedance-research/BFS-Prover

Model

This repository contains the latest tactic generator model checkpoint from BFS-Prover, a…

seewoo5/awesome-ai-for-math

List of awesome works that use AI for mathematical discoveries.

ByteDance-Seed/Seed-Prover

443

RickySkywalker/TheoremLlama

This is the official repository for all the code of TheoremLlama

Languages

Standard ML

59.3%

OCaml

24.9%

Jupyter Notebook

8.0%

Python

7.1%

sean-lamont/bait

Official repository for the AAAI 2024 paper BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving.

Standard ML

253 commits

updated Oct 10, 2025

sean-lamont.github.io/bait

See the code

README

BAIT: Benchmarking Architectures for Interactive Theorem-Proving

BAIT is a platform for accelerating research in the application of AI to Interactive Theorem-Proving (AI-ITP). Please see the website for the complete documentation and more information.

artificial-intelligence

benchmark-framework

machine-learning

theorem-proving

Similar repos

ericjiang18/Awesome-Formal-Mathematics

Xinze-Li-Moqian/awesome-ai4math

The ecosystem reshaping mathematics.

kaiyuy/ASTactic

Model

The ASTactic model in the paper:

drzo/ASTactic

bytedance-research/BFS-Prover

Model

This repository contains the latest tactic generator model checkpoint from BFS-Prover, a…

seewoo5/awesome-ai-for-math

List of awesome works that use AI for mathematical discoveries.

ByteDance-Seed/Seed-Prover

443

RickySkywalker/TheoremLlama

This is the official repository for all the code of TheoremLlama

Contributors

sean-lamont

253 commits

Languages

Standard ML

59.3%

OCaml

24.9%

Jupyter Notebook

8.0%

Python

7.1%