how is lean different from tlaplus for helping you with reasoning during the design phase?

I literally just discovered tlaplus last week after struggling with reasoning about the explosion of permutations about configuration policies Im designing, and Im still learning the math but Im finding it easier to reason with tlaplus than in code is lean like that?

https://www.amazon.com/Maths-Proofs-Lean-First-Steps-ebook/d... I like this author and a while ago found that he'd published a book on Lean!

In the end I wasn't able to read it on my ebook reader and reading it on a PC or smartphone kinda makes it annoying to read on the commute. So I've only read the first two chapters or so but it seemed like a lot of fun. All this talk about using Lean in AI-powered proofs kinda makes me want to pick it up again.

Does anyone do TLA style distributed systems verification with Lean? Curious the experience there and how well supported it is

Just in case anyone else decides to write along like the article suggests. I chose to use the live.lean-lang.org link, but it seems to default to a newer version of lean where the simp[xor] actually returns both sides still wrapped in the lambdas so the next simp[add_comm] will actually fail. The way to get around it is changing the version to v4.32.0 which the article doesn't seem to mention.

I just wish Lean4 is easier to use. Tried Mathematics in Lean and couldn’t even get the dependencies right

Why does Lean always have a way to mess up your file system, writing to any files, rather than just proving proofs?

I found that out when reading the recent articls about counterexamples.

[flagged]