9 repos
Tools and datasets for training language models to perform automated theorem proving, particularly on mathematical libraries like Mathlib. The cluster centers on neural approaches to formal mathematics using transformer-based models, with infrastructure for instruction tuning, context augmentation, and text generation. Most repos are Jupyter notebooks and Python code supporting model training pipelines and theorem proving workflows, often built on PyTorch and Hugging Face transformers.