Visual Studio Code Extension and Language Server Protocol for Coq

Efficient and general syntactical decoding for Large Language Models

Repo-Level Code generation papers

An evaluation benchmark for undergraduate competition math in Lean4, Isabelle, Coq, and natural language.

🍎APPL: A Prompt Programming Language. Seamlessly integrate LLMs with programs.

LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.

Formal representation and solving for Euclidean plane geometry problems.

[COLM 2024] A Survey on Deep Learning for Theorem Proving

[TMLR 2024] G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks

A curated list of resources about generative flow networks (GFlowNets).

Tool for data extraction and interacting with Lean programmatically.

[NeurIPS 2022] "NSNet: A General Neural Probabilistic Framework for Satisfiability Problems"

Retro*: Learning Retrosynthetic Planning with Neural Guided A* Search

A Learning Environment for Theorem Proving with the Coq proof assistant

A research protocol for deep graph matching.