Most purely mathematical statements in TLA+ I know are about basic
properties of
the standard library. You can browse through the _proofs.tla files and
have a
look around.
https://github.com/tlaplus/tlapm/tree/main/library
As Andrew already mentioned proving statements about algorithms usually
does not
rely on complex mathematical results. In a way the construction of the
algorithm
already divides the problem into subtasks that are easier to handle.
cheers,
Martin
On 4/28/24 20:03, marta zhango wrote:
It would help me to have a decently long list of mathematical theorems
(undergraduate mathematics)
proved with TLA+ I can look at. And how to run them and interpret them.
On Monday, April 29, 2024 at 2:15:56 AM UTC+12 Andrew Helwer wrote:
The introductory material for the TLA+ proof system is admittedly not
great at the moment. There is a basic tutorial available on the INRIA
website:
https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/The_example.html
Really though the best way to learn is to just try to prove a very
simple
statement and see how it goes, reading other peoples' proofs for
inspiration. Here are my attempts at some basic proofs:
https://github.com/tlaplus/Examples/tree/master/specifications/LearnProofs
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