Comment by sevenzero

If everything of this can be represented in Lean, with enough compute, they are low hanging fruits, yes