You can also look at the tlaplus/examples repo in general, there is a table in the README with checkboxes marking every spec that includes proofs:
https://github.com/tlaplus/Examples
The TLA+ proof language is usually applied to prove statements that are shallow but broad, as in very simple mathematical statements but a lot of them. This is what you have to do to prove an algorithm correct. Each individual step in the algorithm is usually mathematically simple, but there are a lot of them. I am not aware of the TLA+ proof language being used to prove "deep" mathematical theorems like you hear coming out of the Rocq and Lean community, but perhaps examples exist.
Andrew Helwer
On Sunday, April 28, 2024 at 3:42:08 AM UTC-4 marta zhango wrote:
Felicitations Martin. The problem I struggle with is that the TLA+ book does not cover
the verification of mathematical proofs. purely mathematical. Have scrutinised Stephan's
links to actual
proofs of Cantor's theorem. But can one use the software to show that they
are indeed correct. This is the field of verification that I have interest in at this moment.
Can one find a tutorial about how specific mathematical proofs can be defined and verified ?
Thank you so very much
Marta