LeanFrontier: machine-generated mathematics, verified by the Lean kernel

LeanFrontier is a new Lean 4 library of machine-generated, kernel-verified mathematics. Every theorem it contains has been checked by Lean’s proof kernel rather than taken on faith, which means the machine-generated results carry the same formal guarantees as hand-written proofs.