Presumably made easier by something like Lean where you can have a very minimal set of axioms, because things you might use as axioms already have proved versio

Presumably made easier by something like Lean where you can have a very minimal set of axioms, because things you might use as axioms already have proved versions, in Lean.