|
|
|
|
|
|
by gus_massa
263 days 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? |
|
|
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.