This repository provides a Lean 4 tactic `smt` that automates theorem proving by delegating goals to the cvc5 SMT solver and reconstructing the resulting proof in Lean. It supports a range of theories including uninterpreted functions, linear integer and real arithmetic, bitvectors, strings, and quantifiers. The codebase is organized into preprocessing (normalization, monomorphization, embedding), translation to SMT-LIB, solver communication, and proof reconstruction for each theory. The project is in beta but actively developed, with extensive test coverage across supported domains. While the primary interface is a tactic, the architecture reveals multiple reusable components such as an S-expression DSL, SMT term representation, graph data structure, and a configurable WHNF reduction engine. The main entry point is `Smt/Tactic/Smt.lean`, and the library is distributed as a Lean package. The code is tightly integrated with the cvc5 FFI and Lean's metaprogramming infrastructure, making it primarily a library rather than a standalone application, but it fits the 'application' category as a tool for interactive theorem proving.
This repository is the content generation and build system for the interactive textbook *Mathematics in Lean*. It is a hybrid project: primarily a set of Python scripts and a Lean 4 project that together produce the textbook in multiple formats (Sphinx RST/HTML/PDF), as well as a separate user repository with exercise stubs and solutions. The core pipeline parses Lean source files annotated with custom directives (`TEXT`, `EXAMPLES`, `SOLUTIONS`) via `scripts/mkdoc.py` to generate textbook prose and Lean exercise files. A Sphinx build then produces the final HTML/PDF documentation. The Lean source files themselves cover mathematics from basic arithmetic to measure theory, heavily leveraging the Mathlib library. The repository includes CI/CD workflows (GitHub Actions), developer environments (Devcontainers, Gitpod), and testing scripts that verify the generated Lean files compile. While not a traditional application, it functions as a specialized toolchain for creating and deploying formal mathematics educational content.