Formal Methods @ University of Toronto
LeanEuclid. LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
lean-temporal. Formalization of some temporal logics in Lean
lean-strategies. Lean
lean-algebra. Some formalization of elementary algebra in Lean
