undefined | Better HN

0 pointslitexlang6mo ago0 comments

``` If litex's strategy is "you describe the steps you want to take, and litex will automatically figure out why they're correct", how are you supposed to do any nontrivial proofs? ```

HAHA, what i am saying here is, each statement you write, is automatically checked by Litex, using its known specific facts and universal facts. Since any math proof, no matter complex or simple, can be divided into many small steps and each small step can be verified in that way, I guess it is fair to say "automatically figure out why they're correct" to a non-mathematicl person when introducing Litex.

0 comments

gus_massa6mo ago

How does it escale for NxN system? Let's say N=10 that is the maximal amount I'd write by hand (in exchange for a lot of money).

I took a look at the example and it's very intuitive. I'm trying to guess which heuristics is it using. Does it try to find exact matches of whatever is inside the parenthesis?

@GP?: Doesn't Lean have a "please fill the blanks" mode for short proof?

thaumasiotes6mo ago

> @GP?: Doesn't Lean have a "please fill the blanks" mode for short proof?

Yes, there are several depending on what you want to do. The catchall is `simp` (short for 'simplify').

Why do we need more than one "do what I mean" command? (Or more than zero "do what I say" commands?) Because it's impossible to know what you mean. If you try to use a lot of `simp`, you'll notice that you often have to tell it what to do.

Note that what we really want for this problem is a linear algebra package that can do row reduction, not a formal prover. This problem is all arithmetic.

j / k navigate · click thread line to collapse