TLA+ for testing computational algorithms rather than verify mathematical proofs

[marta zhango‏]

Have been reading the book TLA+ of Hillel.  It is as though TLA+ is only useful

to test computations algorithms.  One cannot test mathematical proofs.  Is this

correct ?

[Martin‏]

Hello Marta!

Showing properties of algorithms is where TLA+ stands out from other logics /
specification languages. The language itself is expressive enough to cover most
of mathematics even when we disregard the temporal aspects though.

Which TLA+ statements we can prove depends on the tools we use. TLC enumerates
all possible variable assignments. It is useful to find counterexamples and
explore problems with finite state spaces. In engineering we might limit ourself
to checking only a relevant finite amount of a problem with an infinite state
space. In that case we don't get a proof of the statement but certainly more
confidence than by classical testing.

TLAPS can prove statements of TLA+ in general, including purely mathematical
statements. For example Stephan's mail yesterday contained links to actual
proofs of Cantor's theorem.

What's so nice about TLA+ is that we can get already very far by just formally
stating the problem and exploring it with TLC. Some people already stop there,
others use TLAPS and add the proofs as well (proving is more time consuming than
writing the problem down after all). That's why you can find both flavours - or
even a mix of them - online.

cheers,
Martin

[marta zhango‏]

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

[Andrew Helwer‏]

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

[marta zhango‏]

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.

[marta zhango‏]

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 problem

of most books and writing being useless in the important parts that get people started

so they can begin doing real work.

[marta zhango‏]

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

[Martin‏]

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

[marta zhango‏]

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

[Martin‏]

To my knowledge TLA+ has not been used to formalize proof of pure mathematics on
the level you aim for yet (in particular not without stating it as an algorithm)
- you would need to build up your proof from the foundations and/or add the
lemmas you trust as axioms. But e.g. the methods of analysis like integrals have
not been formalized yet in TLA+ because noone has needed them so far. In that
regard the interactive provers that aim for mathematics (e.g. Coq, Lean,
Insabelle) might be easier to start with?

cheers,
Martin

[marta zhango‏]

No wonder I could not find anything useful to me.  Will see how I can go with Coq.  Regarging

TLA, I would like to make something similar to what Leslie Lamport has done for mathematical

proofs, even though this was shown before things had been formalized (e.g. as done for The

Mean Value Theorem).

Can I get some help to show that if \sum a_n converges then lim_t^\infty} a_n = 0.

My proof would be to construct a_n = S_n - S_{n-1}

New because \sum a_n converges, then the sequence {S_n}_{n=1}^{\infty} is also convergent

and that \lim_{n=1 \to \infty} s_n = S for some finite value S.

And since n-1 \to \infty as n \to \infty , we also have lim n \to \infty s_{n-1} = S

We now have

lim_n^\infty a_n = lim_n^\infty ( s_n -s_{n-1} )

= lim_n^\infty s_n -  lim_n^\infty s_{n-1} )

= S - S = 0

I cannot do this on my own and need some confirmation that what is produced is correct.

Then I have something that I can build upon.  Could I get some help to do this proof in TLA

in the same manner as Lamport ?