But my quest is to prove statements about mathematics itself (e.g. verifying a mathematical proof
of the linearity of a wavelet transform).
On Monday, April 29, 2024 at 6:20:24 AM UTC+12 Martin wrote:
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
>>>
>>>
>>>
>