I just wish Lean4 is easier to use. Tried Mathematics in Lean and couldn’t even get the dependencies right
Introduction to Formal Verification with Lean Part 1
11–20 of 55 posts
Re: Introduction to Formal Verification with Lean Part 1
#12a) Thanks for putting this together!
b) Please don't hijack my scrolling.
c) I really wish Lean were more mature as an application programming language. Its standard library is really lacking.
Re: Introduction to Formal Verification with Lean Part 1
#13Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/ Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/ And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/ Finally, if this got this even a…
induction b with d hd
rw [add_zero, zero_add]
rfl
rw [add_succ, succ_add]
rw [hd]
rfl
Re: Introduction to Formal Verification with Lean Part 1
#14(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
it's like proof by induction versus trying every number from 0 to infinity
Re: Introduction to Formal Verification with Lean Part 1
#15Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/ Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/ And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/ Finally, if this got this even a…
I love your posts! The Social Filesystem is amazing!
Re: Introduction to Formal Verification with Lean Part 1
#16I built an automated math research system using Lean to verify the results: https://alethean.org
Re: Introduction to Formal Verification with Lean Part 1
#17a) Thanks for putting this together! b) Please don't hijack my scrolling. c) I really wish Lean were more mature as an application programming language. Its standard library is really lacking.
I've often wondered how viable it is to use AI to fill out the ecosystem gaps in awesome but niche languages (still looking at you OCaml...).
I've not gone too deep down this train of thought because a standard library/ecosystem should be solid and I don't think LLMs are quite there... but if we can use LLMs+Lean maybe we can get the quality we need to bootstrap more of the Lean ecosystem?
Re: Introduction to Formal Verification with Lean Part 1
#18I built an automated math research system using Lean to verify the results: https://alethean.org
That is a cool visualization.
Re: Introduction to Formal Verification with Lean Part 1
#19(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
it is very much a related idea. an `assert` statement in e.g. `python` is a statement your code is making about what it means to be correct, and furthermore a statement about what conditions would have to exist to validate the first statement: for example you might need to run it with certain inputs, on a certain file or kind of file.
`lean4` is very much about the same two ideas. you can make statements about what it means for the code to say something interesting, usually something relevant to whether or not it's correct, and you make statements about the circumstances in which you would evaluate that.
people are interested in `lean4` because it allows you to make more interesting statements of both kinds, and you have tools to be much more specific about the details, the `assert` statements in `python` can't really call each other for example, they don't really compose. in `lean4` the ability to compose such statements is very important.
but you can write regular programs in it too. this is a reverse proxy faster than `nginx`: https://cdn.s4.gl/serve-fd.lean
Re: Introduction to Formal Verification with Lean Part 1
#20(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
An assert statement requires that you specifically come up with a test case. Lean lets you verify for all possible cases. Infinity is not a problem.
It's similar to a type system in that regard. The same difference could be applied there (comparing a Python type assert). Types, however, generally only cover checks similar to "the shape of the data is X".
Lean is different in that its language for expressing properties is wide enough to express anything you can imagine. The bottleneck becomes accurately stating properties you'd like to enforce and, subsequently, discovering proofs of whether or not they're true.