4 ms·
As noted in some comments, writing a non-trivial proof by hand with TLA+ only seems possible if there exists a good repository of non-trivial propositions that
by mraison 12y ago
As noted in some comments, writing a non-trivial proof by hand with TLA+ only seems possible if there exists a good repository of non-trivial propositions that one can start from.
Does anyone know of interesting initiatives out there to build an open repository of mathematical proofs?