Conclusion: beyond invariants

We are still lacking:

• A large collection of invariants.
• An estimate for how many implications the resulting metatheorems will settle.
• Algorithms (in Lean, Python, or otherwise) to compute known invariants.
• General results about lifting magmas.
• Formalization of the method of invariants and resulting metatheorems.
• Knowledge about the category-theoretic interpretation of invariants (see the questions in the note for category theorists).

Related to the last bullet point, we note the following. If all that matters about invariants is the fundamental property, we can apply the old French trick of turning a (meta-meta)theorem into a definition.

Q: If we were to define invariants as any functions satisfying the fundamental property, would anything change? (For those who read the note for category theorists: an equivalent redefinition is to consider invariants as functors \(\Pi \to \textbf{Bool}\)).

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.