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

*From*: marta zhango <martazhango@xxxxxxxxx>*Date*: Sun, 28 Apr 2024 11:51:59 -0700 (PDT)*References*: <48640047-49ce-4d12-899b-acea04612b3bn@googlegroups.com> <79520297-12e7-4df4-99d0-51e6b1a1dc40@gmail.com> <e7a7f648-facc-43cb-81e0-21b0f582ea05n@googlegroups.com> <09258c76-5002-45c1-8cb0-0c6996ffd05cn@googlegroups.com> <dfb02434-efb5-47c8-ba25-cbc1992b9ed9n@googlegroups.com> <f47132d0-5022-4284-9d66-19a82ab248fd@gmail.com>

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.

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

>>>

>>>

>>>

>

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.

**Follow-Ups**:**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs***From:*'Martin' via tlaplus

**References**:**[tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs***From:*marta zhango

**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs***From:*'Martin' via tlaplus

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

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

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

**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs***From:*'Martin' via tlaplus

- Prev by Date:
**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs** - Next by Date:
**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs** - Previous by thread:
**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs** - Next by thread:
**Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs** - Index(es):