The essence of mathematical insight often comes from finding a new vantage point.
Vantage envisions a future where mathematical knowledge is navigated as a vast, interconnected graph. This Python project is building the foundations for autoformalization software where each mathematical statement constitutes a node. By employing Lean 4 for rigorous verification and utilizing large language models to drive the autoformalization process, Vantage targets a highly parallelized approach. The ultimate ambition is to map, organize, and accelerate the exploration of the ever-expanding universe of mathematics with unparalleled accuracy and efficiency.
Full Documentation: https://vantageproject.org
For a conceptual overview and the motivation behind this project, see the introductory article: Introducing Vantage.
- Knowledge Base Storage: Stores mathematical items (
KBItem) with code, metadata, and embeddings using SQLite. - Lean Interaction & Persistent Library: Verifies Lean 4 code against an incrementally growing shared Lean library (
vantage_lib) usinglake. - LLM Integration: Interacts with Google Gemini API (async calls, retries, cost tracking).
- Structured Data: Uses Python dataclasses for knowledge representation.
- Dependency & State Tracking: Manages item dependencies and status (
PENDING_LEAN,PROVEN, etc.). - Automated API Documentation: Detailed API reference generated directly from source code docstrings.
- Python: Version 3.8+ recommended.
- Lean 4 & Lake: Working installation with
lakein PATH. (Lean Installation Guide) - Google AI API Key: For LLM features. (Google AI Studio)
The full documentation, including installation guides, usage details, API specifications, and contribution guidelines, is available at:
Key entry points into the documentation include:
- Getting Started: Installation, setup, configuration, and basic usage.
- API Reference: Detailed documentation for all modules and classes.
- Contributing: How to contribute, testing procedures, style guides, and code of conduct.
Vantage is under active development and contributions are highly welcome! If you're interested in helping shape the project, please review the Contributing Guide.
We are actively looking for collaborators! Feel free to explore the issues tab on GitHub, or reach out directly via email at justinchadwickasher@gmail.com with any questions, ideas, or offers to help.
This project is licensed under the terms of the MIT License. See the LICENSE file for the full text.