Zulip Chat Archive
Stream: new members
Topic: Introduction: Rado Kirov
Rado Kirov (Feb 17 2025 at 20:07):
In leau of introduction, I wrote up a quick blog post about my experience finishing Theorem Proving in Lean4 - https://rkirov.github.io/posts/lean1 and has more info about my background.
Kyle Miller (Feb 17 2025 at 20:32):
Re Decidable
, here's another way the class could have been written:
class Decidable' (p : Prop) where
eval : Bool
eval_eq_true_iff : (eval = true) ↔ p
It's a structure that records whether or not the given proposition is true. This lets you lift a given proposition to a boolean value that you can compute with. Propositions themselves do not have any computational content on their own (that's to say, there's no algorithm that can automatically prove that p
is True
or False
), so this is a way to "reflect" logical propositions into a computable form.
The actual docs#Decidable is an inductive type with two constructors; I think of as being a "heavy Bool" that also records what is true or false and why.
(I'm hoping in the future Lean will switch to a variant of Decidable'
. It will help with some definitional equality issues we run into with BEq
.)
Kyle Miller (Feb 17 2025 at 20:38):
Re #eval
vs #reduce
, the first takes the expression, compiles it, and evaluates the compiled code (it doesn't build a binary, but it at least runs the IR (intermediate representation) in a VM). If you #eval
a proposition, it will try to find a Decidable
instance and evaluate the proposition as a Bool
(hence why you see true
and false
rather than True
and False
as the result!).
The second, #reduce
, instead uses the reduction rules of lambda calculus, and symbolically tries to evaluate the expression to normal form. Sometimes #reduce
gets stuck on computations that #eval
doesn't get stuck on. The main difference is that #eval
erases all types and proofs during compilation, essentially simplifying the expression first into an untyped lambda calculus, which is more flexible for computation.
Kyle Miller (Feb 17 2025 at 20:44):
Re simp
: don't confuse it for Simplify[...]
. It tends to simplify, but it's not a simplifier per se. It's a rewrite rule engine, with features that handle applying rewrites deep within expressions automatically (while generating proofs of course!) using so-called congruence lemmas.
The Simplify[...]
function in Mathematica also is a rewrite rule system, but it is actually trying to simplify the expression, and in contrast to simp
it applies its rules nondeterministically (i.e., it explores rewrites along a graph of possibilities). It tries applying a good number of rewrites and then returns the expression it finds that minimizes some complexity measure.
In principle we could (and probably should!) have a Simplify[...]
in Lean, especially with some of the congruence closure modules in the cc
and/or grind
tactics.
Kyle Miller (Feb 17 2025 at 20:46):
Re rfl
and defeq: it's best to use rfl
only if you know the definitions, and you know the definitions are supposed to be unfolded. Breaking through the abstraction barriers with rfl
and forcing a computation (in the #reduce
sense) is sometimes known as a "heavy rfl
".
In large library design, we tend to prefer using rewrite lemmas.
Rado Kirov (Feb 17 2025 at 20:48):
Thanks for all the answers again, it will take me a bit of time to absorb :)
Rado Kirov (Feb 17 2025 at 20:49):
What’s the simplest non decidable prop with Nats? Since decidable is a class, can it be make decidable with an extra instance ?
Damiano Testa (Feb 17 2025 at 20:55):
I do not know if the example below is undecidable in the technical sense (and probably it isn't), but the statement "there are odd perfect numbers" is something for which it would be interesting to have a Decidable
instance!
Damiano Testa (Feb 17 2025 at 20:57):
For an actually undecidable statement, you can look at Hilbert's Tenth Problem.
Rado Kirov (Feb 17 2025 at 20:59):
Yeah that’s what I am struggling with - separating proven to be non decidable in all systems and practically non-decidable because something is missing an type class instance
Kyle Miller (Feb 17 2025 at 21:00):
Along those lines, given an arbitrary function f : Nat -> Nat
, you can't generally decide forall n, f n = 0
. Hilbert's 10th problem is a special case of this, where we restrict the possibilities of f
to be multivariable polynomials (one can encode multivariables polynomials as such an f
).
Kyle Miller (Feb 17 2025 at 21:01):
What would the algorithm be? We could semidecide it by evaluating f
at successive integers, returning false
as soon as we find an n
where f n != 0
. But we can't know for sure that f
is always zero.
Kyle Miller (Feb 17 2025 at 21:04):
For specific examples of f
, of course one can decide whether it's true without needing to fall back on evaluating it over its whole domain. Here's one:
instance : Decidable (∀ n, n * (n - 1) * (n - 2) = 0) :=
isFalse <| by
push_neg
use 3
norm_num
Kyle Miller (Feb 17 2025 at 21:05):
That one would have been semidecided, so here another
instance : Decidable (∀ n, 0 * n = 0) :=
isTrue <| by simp
Rado Kirov (Feb 17 2025 at 21:06):
Perfect that’s helpful, now I wonder for which of the proved props one has to write that instance vs it gets automatically generated because of some type class magic ?
Kyle Miller (Feb 17 2025 at 21:07):
(Complicating things, in Lean every proposition is technically decidable via docs#Classical.propDecidable, but that is noncomputable
and can't be used with #eval
. It uses the docs#Classical.choice to "construct" a decision. There's no code backing that up however, hence the need for the noncomputable
modifier to tell Lean to not try to compile it.)
Kyle Miller (Feb 17 2025 at 21:09):
The typeclass magic consists of a whole library of instances like docs#instDecidableAnd, which can decide p ∧ q
by deciding p
and q
.
Kyle Miller (Feb 17 2025 at 21:10):
The instances syntactically match on the proposition, which is how it can be broken apart and "compiled" into a decision procedure for it.
Rado Kirov (Feb 17 2025 at 21:14):
So if I start building more complicated props when do they stop being decidable - x=y is decidable, adding propositional logic basic ops is too, but is it at first order - existential and universal quantifiers when props stop being decidable or when one uses LEM?
Kyle Miller (Feb 17 2025 at 21:18):
x = y
isn't actually decidable by default -- there's the abbreviation docs#DecidableEq to bring in forall (x y : T), Decidable (x = y)
Aaron Liu (Feb 17 2025 at 21:19):
Actually, x = y
is not always decidable, even for fairly simple constructs. In contrast, every formula in a decidable theory is decidable.
Once you start being able to encode turing machines in your propositions, is when it stops being decidable
suhr (Feb 17 2025 at 21:19):
My main critique is that sometimes it starts using concepts or syntax that was not introduced earlier (the curse of knowledge for the authors).
I would argue this is not because of the curse of knowledge but because authors wanted relatively short and "practical" tutorial. So a lot of essential background is missing.
Kyle Miller (Feb 17 2025 at 21:21):
Rado Kirov said:
existential and universal quantifiers
Yeah, this is a way nondecidability creeps in. Also inductively defined Prop
s in general (Eq
is such an example).
For what it's worth, there are Decidable
instances for quantifiers when the domain is finite (via docs#Fintype).
Rado Kirov (Feb 17 2025 at 21:25):
Ok that is starting to make sense on decidability and gives me enough pointers to look more into it. I see newcomers get tripped on prop vs bool. Funny enough coming from typescript I am very comfortable with that - types are checked and erased, there is no reification at runtime, the whole type language is separately evolved and bolted on a Js runtime. But decidable makes lean not only have that separation but also allow one to bridge it when needed, which is wild :)
Rado Kirov (Feb 17 2025 at 21:28):
suhr said:
My main critique is that sometimes it starts using concepts or syntax that was not introduced earlier (the curse of knowledge for the authors).
I would argue this is not because of the curse of knowledge but because authors wanted relatively short and "practical" tutorial. So a lot of essential background is missing.
I have some concrete example where for example “class … extend …” was used for the first time in a section for another concept and had me “ah type classes can extend like structures” but that wasn’t said directly just used in a fancier example. So not really background. Anyways I will file GitHub issues for those and can discuss them there.
Rado Kirov (Feb 17 2025 at 21:39):
It’s hard to capture how “alien tech” lean feels even for someone that has done programming and math for awhile
suhr (Feb 17 2025 at 22:17):
Yeah, constructive logic turned into a programming language with some extras (like type classes) borrowed from other functional programming languages is not that a classical mathematician or an ordinary programmer is used to see. Though, programmers sometimes play with a lot of weird stuff.
Chris Wong (Feb 17 2025 at 23:15):
Aaron Liu said:
Actually,
x = y
is not always decidable, even for fairly simple constructs. In contrast, every formula in a decidable theory is decidable.Once you start being able to encode turing machines in your propositions, is when it stops being decidable
To give a concrete example:
Equality on real numbers is undecidable. You could have 0.000...
, and without inspecting infinitely many digits, you wouldn't know if it's all zeros (hence equal to 0
), or it actually ends in ...0001
.
Rado Kirov (Mar 03 2025 at 00:38):
Wrote up some more random notes on Lean as I finished first half of MIL - https://rkirov.github.io/posts/lean2/ . It's been lots of fun so far and I have learned a lot from all the conversations happening on here.
Kevin Buzzard (Mar 03 2025 at 08:27):
The links to the puzzle games didn't work for me
Aaron Liu (Mar 03 2025 at 11:07):
It's https://rkirov.github.io/posts/puzzles2024/
Rado Kirov (Mar 03 2025 at 15:21):
ops, fixed the links, thanks for catching that. Speaking of puzzles, I have been wondering how would an even more gamified version of the number game look like - like visually represent inductive types and their reductions though something like moving boxes, etc. Patrick's Parabox is an example of a puzzle game that has non-trivial math content (though not matching any real math theory) as it reifies infinity paradoxes.
suhr (Mar 03 2025 at 15:32):
Theorem proving always reminds me of Baba Is You.
Last updated: May 02 2025 at 03:31 UTC