Recent searches
Search options
#Lean4
Formal Verification for Machine Learning Models Using Lean 4
After months of working daily, today at 5.02pm approx I completed the course
" Mechanics of Proof "
That's means I completed every exercise - (except 3)
When I started I wanted to learn cover the basis of not just algebra, but also sets and functions - and the course does that. The only area it doesn't cover that I wanted was real analysis - eg convergence of sequences etc
phew !
If you think writing maths proofs in code is only for PhDs...
... this course was created for you!
* small bite-size examples
* concepts first, code second
* minimal jargon
* one simple exercise per chapter - designed to build confidence - not destroy it !
My Existential Rule #Lean4 library [1] is taking shape more and more. I've recently finished a correctness proof for a sufficient condition for chase termination, called MFA. I'm hopeful that extensions of this notion (DMFA and RMFA) are not too hard to formalize now once a few ugly technicalities are sorted out :)
[1] https://github.com/monsterkrampe/Existential-Rules-in-Lean
I'm still fumbling about in the dark with Lean, but my goal for my first big project is to implement system F sub omega and prove its type safety. I'm going to try some simpler lambda calculi first, probably, because I fear that which I do not understand.
Question: Does anyone have tips/examples/guides as to how to start to practically describe a type theory? I started out trying to define evaluation and de Bruijn indices etc and got lost in the weeds. Is there a way to operate fully at a higher level, and only really talk about the types? And if I'm only interested in proving the theory, and not with efficient execution, is there a better way for me to represent scopes/contexts?
#Lean4
Feature Request: rofl as alias to rfl
Some strange behaviour with Lean's evaluation of thunks. I wonder if is intentional that this result in [[forcing]] being printed twice?
Keep in mind that if I do a variation on this without using an inductive type constructor, [[forcing]] is printed only once.
"Constructing proofs is an art,
checking them is a science."
If you're new to writing proofs as code, check out my course designed to build confidence - not demolish it!
" 𝗠𝗮𝘁𝗵𝘀 𝗣𝗿𝗼𝗼𝗳𝘀 𝗶𝗻 𝗟𝗲𝗮𝗻 - 𝗙𝗶𝗿𝘀𝘁 𝗦𝘁𝗲𝗽𝘀 " 
Designed specifically for beginners struggling to get started with other courses and guides.
* Simple bite-sized examples.
* Focus on concepts, introduced gradually.
* One easy exercise per chapter.
.. all to build confidence, not demolish it !
... it's out !
" Maths Proofs in Lean - First Steps "
Designed specifically for newcomers and beginners struggling to get started with other courses and guides.
* Simple bite-sized examples explained.
* Concepts introduced gradually.
* One easy exercise per chapter.
.. all to build confidence, not demolish it !
Mario Carneiro, Lean4Lean: Towards a Verified Typechecker for Lean, in Lean - https://www.youtube.com/watch?v=t0kHC0YxjLc
Lean を Lean で形式化することについて。色々と厄介なところがあるんだなあ。
#型理論 #Lean #Lean4 #定理証明支援系
i did a very basic proof for #lean4's batteries module and, despite procrastination on my part, it was merged! https://github.com/leanprover-community/batteries/commit/61dd72099e98719d33239933316e12894677a843
PRs are always nerve-racking for me, but i felt like a million bucks when i got the proof right (i looked at the structure! and did things smart way good!)
@whitequark i don’t really know anything about SMT-LIB but do know something about formal (and first order specifically) logic but this documentation has a long section on quantifiers: https://www.philipzucker.com/z3-rise4fun/guide.html
Then it’s much heavier than an SMT solver but #lean4 is really powerful with good documentation on using quantifiers. I really like it. But it has a heavy emphasis on using tooling and I’m the kind of person who likes rustfmt. https://lean-lang.org/theorem_proving_in_lean4/introduction.html
As a step towards computer-formalizing the classification of low-dimensional Lie algebras, we finally formalized our first non-boring theorem in #Lean4 !
If L is a 3-dimensional Lie algebra (over any field) with a one-dimensional commutator subalgebra which is contained in the center of L, then L is isomorphic to the 3D Heisenberg algebra - that is, it has a basis (𝑒₀, 𝑒₁, 𝑒₂) such that the bracket is determined by
[𝑒₁,𝑒₂]=𝑒₀,
[𝑒₀,𝑒₁]=0,
[𝑒₀,𝑒₂]=0.
Now we're working on the analogous results for higher dimensional commutator subalgebras. These are going to be harder because
a) there's no one-size-fits-all classification statement for arbitrary fields, and
b) they rely on certain normal forms of matrices which aren't yet implemented in #mathlib .
Readings shared January 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/21-readings_shared_01-21-25 #ITP #Lean4 #IsabelleHOL #Math #Prolog #LogicProgramming #AI #LLMs
