By using this site, you agree to our Privacy Policy and our Terms of Use. Close
CaptainExplosion said:
sc94597 said:

Nah, theorem provers that use Lean or Rocq and physically-constrained systems like Alpha Proteo aren't slop. It's because they have ground-truth verifiers and aren't just generating willy-nilly without verification. They also will help a lot of people. 

They don't help artists, animators or writers, they're putting them out of work. -_-

Okay, but Alpha Proteo helps humanity as a whole by expediting the curing of diseases. Theorem provers help humanity as a whole by expediting research that depends on fundamental mathematics. There is more to the world than producing and consuming digital media.