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

*From*: marta zhango <martazhango@xxxxxxxxx>*Date*: Sun, 28 Apr 2024 11:19:02 -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> <91f47544-5f56-4ca5-829c-0b7213c4ccf1n@googlegroups.com>

The examples table in the tlaplus README file are all taken from computer science.

There is no examples of proofs in mathematics (e.g. theorems of number theory, theorems of

sequences and series, real analysis, combinatorics, and similar topics).

On Monday, April 29, 2024 at 6:07:39 AM UTC+12 marta zhango wrote:

The serious problem with the Inria TLA+ Reference is this statement"However, this is a reference manual; you should try some examples before reading it."No examples are ever shown, what example are easy to begin with etc. Same old problemof most books and writing being useless in the important parts that get people startedso they can begin doing real work.On Monday, April 29, 2024 at 6:03:21 AM UTC+12 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.htmlReally 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/LearnProofsYou 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/ExamplesThe 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 HelwerOn 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 coverthe verification of mathematical proofs. purely mathematical. Have scrutinised Stephan'slinks to actual proofs of Cantor's theorem. But can one use the software to show that theyare 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 muchMarta

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/d8a1d5a3-b8f9-48fc-a6e9-b10406309606n%40googlegroups.com.

**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:*marta zhango

- 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):