Comment by carodgers

You might be interested in the con leche project. A subset of the Lean theorem prover which was sufficient to prove the entire contents of Lean mathlib has been proven consistent.