[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs

I understand that proving statements about algorithms does not rely on complex mathematical results.
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.


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.


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

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cdfd7e38-29ee-4b06-b7c5-07e7353f7798n%40googlegroups.com.