CONGRATS! Alexander van der Vekens has proven the Cayley-Hamilton theorem (Metamath 100 #49, total of 72)

[David A. Wheeler]

I want to wish Alexander van der Vekens a big CONGRATULATIONS for proving the Cayley-Hamilton theorem on 2019-11-25!! This is Metamath 100 proof #49.

That brings our "Metamath 100" total to 72. As of 2019-11-25 this number of proofs is more than Coq (69), Mizar (69), ProofPower (43), Lean (29), nqthm/ACL2 (18), PVS (17), and NuPRL/MetaPRL (8); it is short of only Isabelle (82) and HOL Light (86). More info here: http://us.metamath.org/mm_100.html

I've already notified Freek Wiedijk, who tracks progress across various proof systems.

You can see the proof here:
http://us.metamath.org/mpeuni/cayleyhamilton.html

There are still proofs left to do! If you're interested, here's the list of "Metamath 100" proofs not yet done:
http://us.metamath.org/mm_100.html#todo

--- David A. Wheeler

[Alexander van der Vekens]

Thank you, David, for your wishes and your support to publish my contribution. Freek has already updated his web page: http://www.cs.ru.nl/%7Efreek/100/

Alexander

[Alexander van der Vekens]

Benoît proposed to give a bird's eye view of the proof here (a good idea in principle), but I provided already a detailed documentation of the proof in set.mm itself (see comments of subsection "The Cayley-Hamilton theorem"), and I plan to improve/enhance it further in the next days. Hopefully, this documentation will be sufficient. So if you are interested in details, please look at http://us.metamath.org/mpeuni/mmtheorems313.html (caution: this link may not reference the page containing subsection "The Cayley-Hamilton theorem" in the future).

Alexander

[Jon P]

Nice work :)

The lines in the proof are amazingly long. I also think this from the end of line 72 shows some epic nesting "𝑙))))))))‘𝑛))))) = 0 )"

[Alexander van der Vekens]

You are right, the lines in the proof are very long because the definitions (class variables in $e-Statements) of the lemmata used in the proof are expanded (I only kept the definitions which are required to formulate the theorem, not considering the proof...).

Maybe I should provide a second version of the theorem having more definitions, and therefore shorter lines in the proof, so that the proof becomes clearer.

Alexander

[vvs]

We should look at this in the context. I see Metamath as an assembler language, so it's more detailed. If you look at high level tactics language of type theory PAs like Lean and Coq then their proofs may be shorter at the expense of the detail. But if those tactics were expanded then their proofs will become a whole mess which is difficult to understand. So, to be competitive Metamath's proofs should be detailed and clear at the same time. Unfortunately there is no help from available tools to achieve that goals and it's just an art or black magic at the moment.

[David A. Wheeler]

On November 26, 2019 12:36:56 PM EST, vvs <vvs...@gmail.com> wrote:
>So, to be
>competitive Metamath's proofs should be detailed and clear at the same time.

I think that clarity of proofs is important. I think part of the problem is a pair of stylistic conventions, not necessarily weaknesses of Metamath itself.

First, by convention we generally avoid creating new definitions, and I think we currently go a little too far in the direction of avoiding new definitions. There are disadvantages to new definitions, of course. For example, you typically have to have a number of theorems for each new definition so that the definition is useful, and in many cases you still have to expand a definition. Historically another problem was that definitions are really $a statements, which were not checked, but I don't consider that a problem any more (we now have a verifier checking them and I suspect we will have more soon). But new definitions can make more complicated concepts much clearer. If nothing else, new definitions generally shorten expressions and make it clear what the expressions are all about. I think we should seriously consider allowing or even encouraging more definitions so that more complex concepts are clearer. I think everyone agrees that some definitions are important, it's a matter of figuring out where to draw the line.

Second, by convention we often have really long proofs instead of splitting them up into more lemmas and sub lemmas. Splitting them up into logical chunks turn off and really help. I think in at least some cases there are smaller theorems that are both reusable and crying to be made separate.

In the longer term, I'd love to see the work completed to permit portions of proofs to be expanded and hidden while staying on an individual proof. I thought that work was really promising; I don't know what its current status is; I'd love to see that work completed.

There's no getting around the fact that Metamath proofs are going to be much more detailed than many other systems, especially when compared to informal human proofs (such as those in the published math literature). And I can certainly imagine future systems that improve on Metamath. But I think we can use the mechanisms *already* available to make our proofs clearer. Where that makes sense, we should try to do it.


--- David A.Wheeler

[Alexander van der Vekens]

I mostly agree with David,especially that proofs should be clear, comprehensible and as short as possible. I do not fully agree with having more definitions in general. Definitions should be globally meaningful, and not only abbreviations for a single proof/theorem (or a limited group of theorems). In the context of the Cayley-Hamilton theorem, for example, there is an important function I called "characteristic factor function":

G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T `` M ) .X. ( T `` ( b `` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T `` ( b `` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T `` ( b `` ( n - 1 ) ) ) .- ( ( T `` M ) .X. ( T `` ( b `` n ) ) ) ) ) ) ) )

Although having a definition for it would make many proofs in the context of the Cayley-Hamilton theorem clearer, I think there should be no definition using an $a statement for this funtion, because it is unlikely that this function is used elsewhere. On the other hand, I think definitions could (and should) be used more often than in the past.

Concerning splitting proofs in smaller parts, I identified already some interesting, general "theorems" currently embedded in proofs during my work. I plan to extract them (I've just begun with it, see my latest contributions), so that they are generally available, and the corresponding proofs can be shortened. I plan another contribution with such "extracted" proofs in the next days.

Finally, I want to point to the two variants (of proofs) of the Cayley-Hamilton theorem: ~ cayleyhamilton (revised version, using ~ cayleyhamilton0 ), where the $e-Statement definitions used by the lemmata are kept - making the proof more readable, and ~ cayleyhamiltonALT , the original version with the $e-Statement definitions expanded, resulting in very long and not readable lines within the proof.  Maybe these theorems can serve as example for the ongoing discussion about how to use definitions.

-- Alexander

[ookami]

Second, by convention we often have really long proofs instead of splitting them up into more lemmas and sub lemmas. Splitting them up into logical chunks turn off and really help. I think in at least some cases there are smaller theorems that are both reusable and crying to be made separate.

I would love to use lemmas to avoid repeating chunks of proof steps, that are only small variations of each other.  Even in the early parts of Metamath there are dozens of examples, where such repetitions litter up the overall idea of the proof.

Wolf

[Benoit]

As for definitions: it looks like Alexander was referring mainly to $e-statements which serve the purpose of local definitions, while David talked mainly about the $a-statements.  As for the $e-statement definitions, they can serve as definitions used in the statement of the theorem, or only in its proof.  They can be removed easily: I added two theorems a few months ago to illustrate this:
   http://us2.metamath.org/mpeuni/bj-pwcfsdom.html
   http://us2.metamath.org/mpeuni/bj-grur1.html   (the comment there should read "grur1" and not "grur1a")
where I call these hypotheses respectively "definitional hypotheses" and "proof-facilitating hypotheses".

Alexander: it might be possible, similarly, to use one version of cayleyhamilton to prove the other, instead of having two very similar proofs.

As for lemmas: I agree that they could be more used.  It can even be rewarding to extract such lemmas.  I experienced this recently after noticing that two proofs were nearly identical, and searching precisely what they had in common, before extracting it as a separate theorem (this is http://us2.metamath.org/ileuni/peano5set.html with its two uses).

Benoît

[David A. Wheeler]

On November 27, 2019 4:04:11 PM EST, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
>... I do not fully agree with having more definitions in general. Definitions should be globally meaningful, and

>not only abbreviations for a single proof/theorem (or a limited group of
>theorems).

Fair enough. I agree that in Metamath definitions should be more broadly useful, not something only useful a few times. I just think we sometimes shy away from creating definitions even when they *would* apply to many theorems.

This appears to be an advantage of Metamath Zero, which permits local definitions (unlike straight Metamath). The newer "operation" variables of set.mm, like plus-with-broken-underline, do help.

None of this is meant to take away from your success!!


--- David A.Wheeler

[Benoit]

Alexander,

I'm looking at the section comment of "21.25.10.3  The Cayley-Hamilton theorem".  What is the metamath label corresponding to Equation (2) ?  I see that ~cramer has no theorem referencing it.  I thought the natural proof of (2) would use Cramer's rule ?

Thanks,

Benoît

[Alexander van der Vekens]

Hi Benoît,

the metamath theorem corresponding to equation (2) (called "fundamental relation of the adjugate" in Wikipedia) is ~ cpmadurid (see step 7. of the outline of the proof), which itself is a special case (for the characteristic matrix of a matrix) of ~ madurid , contributed by Stefan O'Rear  in July 2018.

So this theorem was already proven before Cramer's rule was available (which I proved in Februrary this year).  I used ~ madurid indirectly for the proof of Cramer's rule (via ~ matinv , ~ matunit , ~ slesolinv , ~ slesolinvbi , ~ slesolex and ~ cramerlem3 ). This is the reason why Cramer's rule is not required to prove the Cayley Hamilton theorem.

Regards,

Alexander