In "laymans" terms, it gives you a) an environment for ML models to verify their proofs and b) and rich space for ML to study relations between different fields of mathematics, logic, philosophy, ethics, and everything else by default at that point.

propositions are implementations of types so just being able to say when propositions are equivalent in like a rigorous way is good for science anyways.