5 Comments

  1. I don’t think the reporting is accurate. The models are not themselves proving theorems. The models are usually paired with lean or other proof languages and iteratively changing the outputs until something valid comes out.