Blaster provides an SMT backend for Z3 proofs. Blaster works by first aggressively optimizing the Lean expression of a theorem, sometimes up to a True goal, before sending the remaining goal and context to an SMT solver.
Blaster is built with the philosophy that fewer dependencies mean better maintainability and more optimization opportunities. That said, Blaster requires:
- Lean4 v4.24.0 (or compatible version)
- Z3 v4.15.2 (or compatible version)
We strive to stay in sync with the latest stable release of Lean4.
Currently supported version: Lean4 v4.24.0
Please follow the official installation guidelines from the Lean4 GitHub repository.
We do our best to stay updated with the latest release of Z3. However, regressions can occur and often require extensive research and resolution, so Blaster might be slightly behind the latest version.
Currently tested version: Z3 v4.15.2
Note: Blaster should work with later releases, though no guarantees are made.
Please follow the official installation guidelines from the Z3 GitHub repository.
Coming soon: Detailed feature list
Blaster has been benchmarked against a variety of well-known benchmarks to evaluate its performance and correctness.
Lean Natural Number Game
- Repository: [Add link here]
- Results: [Add results here]
Lean Set Theory Game
- Repository: [Add link here]
- Results: [Add results here]
Verina.io
- Repository: [Add link here]
- Results: [Add results here]
"Lean-Book"
- Repository: [Add link here]
- Results: [Add results here]
We welcome all contributions! Whether it's bug reports, feature requests, documentation improvements, or code contributions, your help is appreciated.
Please see our Contributing Guidelines for more information on how to get started.
- Report bugs and issues
- Suggest new features or improvements
- Improve documentation
- Submit pull requests
Maintained by:
Questions? Feel free to open an issue or reach out to the maintainers.