Crowdsourcing the proof of 1729 != 817

Stream: Equational

[Terence Tao]

Hello everyone! In this post, I am hoping to start a push to finish off the last remaining task in the original EquationalTheories project, which is to show that 1729 does not imply 817. This is the most complex proof of a single refutation in the entire project; see the blueprint chapter.

The first step - Theorem 18.1 - is currently being worked on by @Shreyas Srinivas. This reduces matters to constructing some objects SM, N, R', L', S', op obeying certain axioms. The next steps are to construct some of these objects, and reduce to a fresh set of axioms. Specifically, one has

• equational#1105 - establish the basic properties ofSM - already defined in the repository
• equational#1106 - establish the basic properties of N - already defined in the repository
• equational#1107 - establish the basic properties of R' (and its inverse) - already defined in the repository.
• equational#1108 - express L' in terms of a single map L₀' and establish basic properties
• equational#1109 - rewrite axioms in terms of L₀'

The first three tasks are relatively easy and should be independent of each other. The fourth task may possibly depend slightly on the third, and the fifth may depend on the fourth as well as @Shreyas Srinivas 's task. Anyway, I am hoping that people will be able to take up these tasks and complete them relatively soon. Please feel free to "claim" one of these tasks on the Github issues page at https://github.com/teorth/equational_theories/issues

This takes us about halfway to the proof; the second half is then to use a greedy algorithm construction to build objects L₀', S', op obeying the remaining axioms. I'll make tasks for those shortly, but wanted to start with these (somewhat easier) tasks to make sure the workflow is adequate.

[Shreyas Srinivas]

The fourth task can be done without any further input from my side since only the ExtWithProps structure is needed to fetch the properties

[Terence Tao]

It turns out that it was easy to establish that SM and N were Countable from Mathlib (essentially immediate from instCountableDFinsupp and Quotient.countable); I've uploaded the proof and removed those tasks from equational#1105 and equational#1106, so one only needs to verify the purely algebraic facts about these two spaces now.

[Terence Tao]

equational#1105 and equational#1107 were in fact rather easy and are now completed. I've added tasks for all the remaining portions of the 1729 implication, feel free to claim any one of them! (In principle they can all be worked on independently, provided that I have written all the definitions correctly...)

[Bernhard Reinke]

I think I managed to do equational#1106. I also proved some instances of order properties that are implicitly used later in the proof (namely, every element of N has only finitely many predecessors, and the largest of them is the "parent"). I hope this is enough for the partial order on N, if something should be added at this part, please let me know!

[Terence Tao]

Thanks, this is great! Good to see that the existing library on lists is extensive enough to make this task relatively straightforward.

There might be two additional facts needed for Proposition 8.14: parent x ≤ x and adjacent x y → x = parent y ∨ y = parent x. Also adjacent x y ↔ adjacent y x could be handy (and presumably very easy to show). If these could be added (either with proofs, or with sorries to set a new task for) that would be helpful, thanks!

[Terence Tao]

@Shreyas Srinivas I'm halfway through establishing reduce_to_new_axioms and am trying out your API. Mostly it is going well, there are just a few technical issues I encountered:

• In ExtOps I think the EM field is unnecessary (and also a weird type, it is currently asking for a specific element of  SM ⊕ N).
• Your types injective, surjective, bijective, Invertible are largely covered by the existing types Function.Injective, Function.Surjective, Function.Bijective, Equiv respectively. Related to this, I think the bij component of Invertible is redundant (it is covered by Equiv.bijective).

[Shreyas Srinivas]

I added those because I am counting on sum types to get injectivity by default

[Shreyas Srinivas]

At least some of those definitions were defined on set maps.

[Shreyas Srinivas]

Yeah I can remove EM

[Shreyas Srinivas]

Its' not necessary

[Shreyas Srinivas]

However SM ⊕ N is just Sum SM N

[Shreyas Srinivas]

Which is the final magma that will satisfy 1729 and refute 817. It's the type theorists way of saying "Here is a disjoint union of two types"

[Shreyas Srinivas]

I figured it would be much simpler to define extension functions on types than sets.

[Terence Tao]

I think the Mathlib types Function.Injective etc. do not use Set. I agree with the use of Sum. Though I will point out that ExtOpsWithProps.sqN_extends_sqM is a tautology (it is proven by intro _; aesop) and does not need to be data (as with Injective.bij).

[Shreyas Srinivas]

It's the inverse that is set theoretic

[Shreyas Srinivas]

The inverse map is basically mapping and x in the range to its pre-image (which is defined as a set).

[Terence Tao]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Equiv/Defs.html#Equiv also does not use Set

[Shreyas Srinivas]

Ah I see you are talking about a different inverse definition. I'll quickly refactor to use that

[Shreyas Srinivas]

Btw, I am filling out 18.1 here: https://github.com/teorth/equational_theories/pull/1133

[Terence Tao]

Hmm, I'm realizing I should refactor R'_inv and L'_inv using Equiv as well

[Shreyas Srinivas]

My main objection to use Equiv is that it is a statement that two types are equivalent without paying heed to what the function is

[Terence Tao]

Equiv.toFun is the function

[Shreyas Srinivas]

Since our claims are that N is equivalent to N, even the identity function will satisfy it

[Shreyas Srinivas]

Whereas in my statement, I am claiming that f is invertible and there is a specific inverse for f

[Shreyas Srinivas]

I don’t know how much difference this makes in the formalisation

[Terence Tao]

Yeah that's Equiv.toFun and Equiv.invFun. It's part of the data of Equiv

[Terence Tao]

It's not just a Prop, it carries this information

[Shreyas Srinivas]

Okay. I'll push the refactoring to equational#1133

[Terence Tao]

Equiv is basically identical to your Invertible, except that it already comes with a full API, and that Injective.bij has been moved out of the data of the type and become Equiv.bijective instead

[Shreyas Srinivas]

Shreyas Srinivas said:

Okay. I'll push the refactoring to equational#1133

done

[Shreyas Srinivas]

Basically the ExtWithProps structure only contains the axioms with the exception of the squaring_map, left_map and right_map properties.

[Bernhard Reinke]

Terence Tao said:

Thanks, this is great! Good to see that the existing library on lists is extensive enough to make this task relatively straightforward.

There might be two additional facts needed for Proposition 8.14: parent x ≤ x and adjacent x y → x = parent y ∨ y = parent x. Also adjacent x y ↔ adjacent y x could be handy (and presumably very easy to show). If these could be added (either with proofs, or with sorries to set a new task for) that would be helpful, thanks!

I have added them as well with proofs

[Terence Tao]

Wow, that was fast! One more subtask completed...

[Terence Tao]

equational#1109 is now completed (some slight refactoring will be needed when equational#1133 lands, but it should be straightforward).

[Terence Tao]

equational#1116 (direct limit of an asymptotically complete chain of partial solutions is a complete solution) is now also completed. I discovered numerous typos in my definition of a partial solution, but of course part of the point of formalization is to weed them out. Also I found that filter_upwards was a convenient tactic to do these sort of direct limit arguments.

I'll start on equational#1120 (the endgame, using the three enlargement propositions to create an asymptotically complete chain of partial solutions) next. After that, the only things that need to be established are Theorem 18.1 (which equational#1133 is addressing) and the three enlargement propositions (equational#1117 equational#1118 equational#1119), which can be worked on independently.

[Terence Tao]

equational#1120 is completed. exists_greedy_chain is well suited for greedy arguments with multiple different ways to extend the object (though I had to refactor the use_chain lemma to actually use chains, rather than enumerating by Nat).

[Shreyas Srinivas]

one half of theorem 18.1 is done. I'll finish the other half tomorrow.

[Shreyas Srinivas]

I might need to carefully look at some of the axioms again

[Shreyas Srinivas]

quick question : what is reduce_to_new_axioms meant for?

[Shreyas Srinivas]

I am refactoring that file to fix the breakages from changing the Ext structure to use Equiv

[Terence Tao]

It formalizes Lemma 18.9, converting the axiom set in Theorem 18.1 to a slightly different axiom set in which all the left multiplications L' a are modeled by a single function L₀'.

[Terence Tao]

Among other things it will need additional code to verify axiom vii

[Terence Tao]

but the Equiv stuff should actually be shorter because L' and R' also use Equiv

[Shreyas Srinivas]

Can’t we just define L’_0 with the magma operation?

[Shreyas Srinivas]

From 18.1

[Terence Tao]

That would be circular. Theorem 18.1 needs to specify L' as one of the inputs to build the magma operation, and L' is constructed using L₀'. A posteriori, L₀' is leff multiplication by 0, but we can't use that fact until after the magma is constructed.

[Terence Tao]

the arrow of causality is (new axiom set (iii')-(vii')) =Lemma 18.9=> (initial axiom set (i)-(vii)) =Theorem 18.1=> (1729 counterexample magma)

[Shreyas Srinivas]

Oh I see now 18.9 is dealing with our specific extension strategy

[Terence Tao]

finished equational#1117. A ridiculous amount of API was needed in order to formalize and then manipulate "does not appear as a component of any index of any of the generators e a appearing anywhere in the partial solution", but now this is in place, the two remaining tasks equational#1118 equational#1119 should be relatively straightforward.

[Alex Meiburg]

That problem sounds familiar. :smiling_face_with_tear:

[Alex Meiburg]

It makes me wonder/wish if there was some better higher-level API for describing such a thing.

[Terence Tao]

finished equational#1119. Tedious, and there were some minor issues that required updating the blueprint and doing some technical refactoring of other parts of the agument, but no major speedbumps. Now down to just two tasks - Theorem 18.1 and Proposition 18.14!

[Terence Tao]

I'm realizing that one of the final tasks, equational#1118, is actually rather massive. As I think about how to formalize it, I see that I can spin off smaller subtasks that can be worked on separately by others. I have created the first such task at equational#1140. The task is to somehow use induction to get from

lemma enlarge_S'_induction {sol : PartialSolution} {x:N} (hind: ∀ y:N, y < x → y ∈ sol.Dom_S') : ∃ sol' : PartialSolution, sol ≤ sol' ∧ x ∈ sol'.Dom_S' := by sorry

to

lemma enlarge_S' (sol : PartialSolution) (x:N) : ∃ sol' : PartialSolution, sol ≤ sol' ∧ x ∈ sol'.Dom_S' := by sorry

@Bernhard Reinke has kindly supplied instance : LocallyFiniteOrderBot N already (and PartialSolution has an instance of PreOrder), so this should be straightforward, hopefully by an induction tool already present in Mathlib, but I haven't seriously attempted to locate it. Anyway, this should be a bite-sized task that anyone who is somewhat familiar with the order-theoretic portion of Mathlib should be able to finish off without having to grapple with the hairy details of how to prove enlarge_S'_induction.

[Terence Tao]

The second bite-size task is equational#1142. Here, the task is to get from the already-formalized

lemma enlarge_L₀' (sol : PartialSolution) (x:N)  : ∃ sol' : PartialSolution, sol ≤ sol' ∧ x ∈ fill sol'.Predom_L₀'

to

lemma enlarge_L₀'_multiple (sol : PartialSolution) (A: Finset N)  : ∃ sol' : PartialSolution, sol ≤ sol' ∧ A.toSet ⊆ fill sol'.Predom_L₀' := by sorry

An induction on the cardinality of A should work here, and one does not need to know anything about PartialSolution or the proof of enlarge_L₀' other than that PartialSolution has an instance of PreOrder. (So perhaps one could create a more abstract, Mathlib-suitable lemma to formalize the general induction argument, and then specialize to this particular setting.)

It may also be possible to use the existing tool https://teorth.github.io/equational_theories/docs/equational_theories/Mathlib/Order/Greedy.html#exists_greedy_chain .

[Terence Tao]

A third bite-size task is equational#1144. Here, the task is to use the two lemmas

lemma enlarge_L₀'_multiple (sol : PartialSolution) (A: Finset N)  : ∃ sol', sol ≤ sol' ∧ A.toSet ⊆ fill sol'.Predom_L₀' := by sorry

lemma enlarge_S'_induction_with_axioms {sol : PartialSolution} {x:N} (hind: ∀ y:N, y < x → y ∈ sol.Dom_S') (hA: ∀ a, R' a x = parent x → R' (sol.S' (parent x)) x ∈ sol.Dom_L₀') (hB: ∀ a, x = R' a x → R' (S (a - sol.S' (parent x))) x ∈ sol.Dom_L₀') (hC : ∀ y z, (x,y,z) ∈ sol.I → z ∈ sol.Dom_S' → R' 0 ( R' (sol.S' z) x ) ∈ sol.Dom_L₀') : ∃ sol', sol ≤ sol' ∧ x ∈ sol'.Dom_S' := by sorry

to obtain the conclusion

lemma enlarge_S'_induction {sol : PartialSolution} {x:N} (hind: ∀ y:N, y < x → y ∈ sol.Dom_S') : ∃ sol', sol ≤ sol' ∧ x ∈ sol'.Dom_S' := by sorry

Basically enlarge_S'_induction_with_axioms is the same as enlarge_S'_induction but with additional axioms about the domain sol.Dom_L₀' of the function sol.L₀'. Once one verifies that the number of such axioms is finite, one should be able to directly appeal to enlarge_L₀'_multiple to conclude. (The prior task equational#1142, which formalizes the proof of enlarge_L₀'_multiple, can be done independently of this one.)

[Terence Tao]

I am belatedly realizing that much of the tedious nature of the already formalized portion of the proof here could have been alleviated if I had incorporated inductive types more systematically into the constructions (particularly with regards with all the times one extends various partial functions). Well, at least I get to learn how to use inductive types properly now in the home stretch of the proof.

[Shreyas Srinivas]

That comes with disadvantages if the blueprint is set up in a set theoretic way. It is easy to say that one “extends a map” in naive sets and that might look easy in inductive types, but over time, the objects in the set get buried under more and more constructors with each extension

[Shreyas Srinivas]

In principle one could also use functions that map to option types, but extending them means adding a layer of if statements each time.

[Terence Tao]

So far what inductive types have allowed me to do is to defer the most combinatiorially involved part of the verification, namely the "no collision" aspect of the extension, which basically comes down to a certain matching map from the inductive type to be injective. Assuming that for now, I can define a preliminary extension on the inductive type, and use some combination of Exists.choose and if _ then _ else to then give a putative version of that extension on the original domain, and use the aforementioned injectivity properties to show that that extension behaves as expected. It's possible that this could be streamlined with some API (I need to extend four separate functions, so it's almost worth it to abstract this out) but so far it is reasonably manageable.

I am slightly nervous about verifying the injectivity; after breaking up into cases, I am looking at dozens of statements to the effect that certain words in the free group cannot equal other words in the free group, with the main justification being that one of them involves a "fresh" generator that does not appear in the other. But I'm working my way through the other parts of the verification now and at the end I should have an explicit list of all these sorts of statements that require proof, at which point it should be clearer how next to proceed. (For instance, of the nine axioms I need the extension to verify, I have already established the three easiest ones, conditional on these sorts of injectivity properties and their basic consequences).

[Shreyas Srinivas]

With inductive types you get injectivity for free upto constructors

[Shreyas Srinivas]

there is the injection tactic to falsify equalities between objects built from different constructors

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

you could try something like cases h : <object> (try injection at <equality hypothesis>) with ...

[Shreyas Srinivas]

This will attempt to apply injection to all the cases.

[Shreyas Srinivas]

For rcases the syntax would be more like rcases h : <object> <;> try injection at <equality hypothesis> ...

[Terence Tao]

That might be useful, thanks. For now I am focusing on developing some abstract API for editing operations: given an initial function f : X → Y, an embedding ι : X' ↪ X, and a replacement function
f' : X' → Y, create a new function edit f ι f' : X → Y which replaces f ι x' with f' x' for all x' : X'. In the applications, X' will be an inductive type which maps to the base type X; the no-collision aspect is then hidden in the embedding property.

[Shreyas Srinivas]

@Terence Tao : In type theory lingo you are extending f to a sum type

[Shreyas Srinivas]

I have already done this my PR

[Shreyas Srinivas]

It's at the very beginning

[Shreyas Srinivas]

Specifically

def extend_sum_inl (f : α → β) (γ : Type) : α → Sum β γ :=
  fun (x : α) => .inl (f x)

def extend_sum_inr (f : α → γ) (β : Type) : α → Sum β γ :=
  fun (x : α) => .inr (f x)

def combine (f : α → β) (g : γ → β) : Sum α γ → β :=
  fun x =>
    match x with
    | .inl xl => f xl
    | .inr xr => g xr

def extend_sum_both (f : α → β) (g : δ → γ) : Sum α δ → Sum β γ :=
  let f₁ := extend_sum_inl f γ
  let g₁ := extend_sum_inr g β
  combine f₁ g₁


def is_left_extension_of (f' : α → γ) (f : α ⊕ β → γ) : Prop :=
  ∀ x : α, f' x = f (.inl x)

def is_right_extension_of (f' : β → γ) (f : α ⊕ β → γ) : Prop :=
  ∀ x : β, f' x = f (.inr x)

[Shreyas Srinivas]

The embedding is injective by definition since on the respective domains and ranges it is the identity function

[Shreyas Srinivas]

One can of course generalise these definitions to arbitrary embeddings

[Shreyas Srinivas]

The generalised version of extend_sum_inl and extend_sum_inr would be something like:

def extend_sum (f : α → β) (embed : β ↪ Sum β γ) : α → Sum β γ :=
  fun (x : α) => embed (f x)

But I suspect this generality is excessive for our situation where we preserve existing mappings and merely extend them, and my definitions capture this whereas this general definition doesn't.

[Shreyas Srinivas]

theorem 18_1 is down to its last sub case

[Terence Tao]

It's possible that combine could be replaced by docs#Sum.elim to take advantage of the API in the latter.

I ended up developing my own API for the ability to "edit" a function using an embedding, in https://github.com/teorth/equational_theories/blob/main/equational_theories/ManuallyProved/Equation1729/Edit.lean , which has made things relatively painless (subject to establishing the injectivity property Function.Embedding.inj' of various maps needed in the construction, which I have deferred for now). Of the nine axioms I need the construction to verify, five verifications have been formalized modulo this injectivity; I will work on the other four next, and then finally get around to checking all the injectivity or "no collision" hypotheses.

[Shreyas Srinivas]

I looked at that file and although I haven't tried this (so evidence is slim), I think the type theoretic versions of these definitions will be much easier to work with, lean-wise.

[Shreyas Srinivas]

Also, I notice you are getting into the gnarly world of Finsets and Fintypes

[Terence Tao]

After looking through Mathlib I see that I should probably have made the design choice at the beginning to use docs#PFun to model all the partial functions used in a partial solution. The editing notion I was developing is then a combination of (a) the operation of pushing forward a partial function by an embedding, and (b) gluing together two partial functions with disjoint domains of definition. But at this point I am a thousand lines of code into the proof, and this is the last time we will use these notions, so I am not inclined to do a major refactor at this point (I already had to do a number of smaller, but still quite time-consuming, refactors, to fix some typos in the blueprint, most annoyingly I had been inconsistent abut whether to use left multiplication or right multiplication on N to define various operations).

[Terence Tao]

Completed the most delicate part of equational#1118 - verifying that the construction (which I was finally able to describe in a civilized way using inductive types and some "editing" API) preserves the axioms, assuming that various "no collision" injectivity type statements are verified (which amounts to a large number of case checking that certain expressions in the free group do not evaluate to equal other certain expressions in the free group). I am deferring all of these to the end, but am finding that some of them can be concatenated into a single claim.

There were numerous typos in the blueprint that were picked up during this process, in a fashion that would not have been possible without extremely careful human line by line reading. Some required nontrivial modfication to the setup (in particular, I discovered the need for a new axiom, which is now in the blueprint as "axiom P'", though it was fortunately preserved by the construction). The most annoying one was that I realized that I had implemented the construction to use left multiplication on the free group for one half of the argument and right multiplication for the other half. The refactoring was quite tedious (in particular, I made the wrong choice initially and attempted to refactor the part of the code that involved lists, which I only belatedly realized did not have a fully symmetric API with respect to heads vs. tails of the lists, so I reverted and instead refactored the part involving free groups, which was much more symmetric).

When I first started coding this task, I placed everything inside one giant lemma, which eventually acquired quite a few let and have statements. This was initially convenient, but VSCode started choking on my basic laptop after a couple hundred lines of code in, so I eventualy ended up spinning off most of the setup into external abbrev and lemma statements instead (I had resisted this initially because most of my constructions required bespoke parameters and hypotheses defined inside the giant lemma, but I finally realized that I should embrace polymorphism and extend the notion of a partial solution to incorporate this additional data, at which point all the setup could be moved outside without difficulty.) This created a noticeable speedup in the Lean infoview response time, which was quite essential for me as I had to do some quite delicate parsing in order to close off the dozens of case checks required.

[Terence Tao]

If I had to start over, I would have coded all partial functions, such as a partially defined squaring map S: N → SM on some domain dom_S: Finset N (with junk values outside of this domain), instead as a globally defined map S: Option N → Option SM, with an additional axiom S ⊥ = ⊥ as well as a Finsupp type hypothesis, with some API to "Optionize" a globally defined function. (There already is support for partial functions in docs#Pfun, but for this specific application, in which one is always composing together many partially defined functions, the above choice seems slightly more convenient.) The current code has to keep track of whether various substrings of expressions live in their indicated domain, and the Option mechanism seems to track that quite neatly with less bookkeeping. But at this stage I'm just going to go with the current framework as the refactor would likely be extremely massive and lead to no long-term time savings since this is the last of the "Greedy algorithm" arguments to be finalized.

[Terence Tao]

On a much more minor note, I am appreciating the use of the symbol $ to declutter a long string of compositions of functions, and am beginning to also take advantage of ▸ to declutter a long string of rewrites.

[Shreyas Srinivas]

I prefer <| for that purpose since it shows you that the right hand side is being applied to the left

[Terence Tao]

A new bite-size task: equational#1151, which asks to prove that the free group is torsion-free.

lemma FreeGroup.torsionfree {α : Type*} [DecidableEq α] : Monoid.IsTorsionFree (FreeGroup α) := sorry

We already have the Nelson-Schreier theorem in subgroupIsFreeOfIsFree, so this should be a straightforward corollary once one understands the API for free groups and IsTorsionFree.

[Bernhard Reinke]

We proved this already in ForMathlib/GroupTheory/FreeGroup/ReducedWords.lean, you can either use FreeGroup.infinite_order or FreeGroup.zpow_injective

[Bernhard Reinke]

see equational#1153

[Terence Tao]

Thanks, this is great! In retrospect it makes sense that you would already have encountered this.

[Terence Tao]

A somewhat annoying update: the process of verifying the non-collision properties required to finish off the 1729 argument revealed that, under the current axiom system of a partial solution, some bad collisions can in fact occur. I can fix this, but only by adding three more axioms to the axiom system, which will greatly delay the completion of the formalization. In a way, this is a win for formalization, as there were about 80 (!) or so non-collision cases to check and it is quite likely that a pen-and-paper verification would have missed the handful of bad cases; but it does mean I am going to spend a lot more time on this than I had expected.

[Shreyas Srinivas]

as far as I can tell, axiom 5,6 and 7 don't seem to be a complete enough description of the rest_map

[Shreyas Srinivas]

This is where 18.1 is stuck right now

[Terence Tao]

axiom 7 should have an \and instead of an \implies:

axiom_7 : ∀ x y : N, ¬ x = y -- the condition for axiom 5 doesn't hold
    → ¬(∃ a : SM, x = R' a y) -- the condition for axiom 6 doesn't hold
    → (∃ z, rest_map x y = .inr z -- for any `z` of this form
      ∧ rest_map z x =  (Sum.inr <| (L' (S' x)).symm y))

one can then use Exists.choose to control rest_map

[Shreyas Srinivas]

Ah that makes more sense

[Shreyas Srinivas]

Yeah that case was simple. I just have one niche sub sub sub case left

[Shreyas Srinivas]

It can be "solved" by assuming the following : ((E.R a).symm (E.S' x')) = (E.L (E.S' x')).symm a) Nvm, I had an idea by just writing it out

[Shreyas Srinivas]

This assumption should work: \E.R a = E.L (E.S' x')

[Terence Tao]

This is an odd condition. What is the sub-case that is triggering it?

[Terence Tao]

Oh crap I think there is a typo in axiom iii... I am double checking now but it looks like $R_{S' x}^{-1} a$ should be $L_{S'x}^{-1} a$. This is going to cause a number of other issues in the rest of the proof, but let me first double check

[Terence Tao]

OK It should be fine if one replaces axiom_3 with

axiom_3 : ∀ x y, ∀ a, R' a x = y → ((L' (S' y)) (L' ((L (S' x)).symm a) y)) = x

Let me know if that works. It will cause some local changes to the proof of reduce_to_new_axioms but it should not be bad because SM is commutative (in the model used there) and so L and R are in fact identical.

[Terence Tao]

Again this is why we need formalization for this sort of project!

[Shreyas Srinivas]

Just got back. I will check the new version

[Shreyas Srinivas]

18.1 is done. All that remains is fixing the downstream consequences

[Shreyas Srinivas]

in 18.9

[Terence Tao]

Do you want to have a try at that, or you can instead put in relevant sorries in reduce_to_new_axioms to close out the PR and I can go through it later.

[Shreyas Srinivas]

I think I can do it, but it makes sense to create a separate PR for it anyway

[Shreyas Srinivas]

I'll just sorry out everything for now in this PR

[Terence Tao]

OK so then you can merge your current PR as soon as it passes CI

[Shreyas Srinivas]

Okay. This should make the Equiv based definitions available for downstream PRs right away

[Shreyas Srinivas]

done

[Pietro Monticone]

@Shreyas Srinivas Did you push your entire Python virtual environment?

[Shreyas Srinivas]

Let me check

[Shreyas Srinivas]

I should have the same gitignore as the main repo

[Pietro Monticone]

There's a huge diff.

[Shreyas Srinivas]

Oh then that must be me

[Shreyas Srinivas]

Isn't the python venv folder in .gitignore by default?

[Pietro Monticone]

Sure, but it seems you added a bin folder.

[Pietro Monticone]

Please consider reverting the commit, restoring the merged branch, removing those unnecessary additions and merge the PR.

[Shreyas Srinivas]

alternatively I could git rm the bin folder

[Pietro Monticone]

There is much more than that (see this, this, this). I think it's better to revert the commit to be 100% sure.

[Shreyas Srinivas]

I am currently not on my laptop. Could you do this fix for me? The PR needs to be re-merged after getting fixed since downstream PRs will depend on it

[Pietro Monticone]

Ok, I'm going to revert the latest commit.

[Shreyas Srinivas]

Also, we need to update .gitignore and push it so that it ignores everything related to python venv

[Pietro Monticone]

Reverted. I'm going to update the .gitignore

[Shreyas Srinivas]

The most likely source of these files is me compiling the blueprint locally yesterday

[Pietro Monticone]

Could you please just locally aggregate all those folders within the usual .ven folder?

[Shreyas Srinivas]

Sure

[Pietro Monticone]

Great, so we don't need to add anything non-standard to our .gitignore. Thanks.

[Pietro Monticone]

I'm going to open a new PR with those additions then.

[Shreyas Srinivas]

no not necessary

[Shreyas Srinivas]

we can simply reset to a few commits before

[Shreyas Srinivas]

and then replay the changes from the local copy

[Shreyas Srinivas]

Also, in general we should avoid re-PRing since we are using PRs for authorship descriptions

[Pietro Monticone]

Ok, I restored the branch you used for the PR.

[Shreyas Srinivas]

okay I will redo it

[Shreyas Srinivas]

Done : https://github.com/teorth/equational_theories/pull/1154

[Shreyas Srinivas]

Just replayed the history in a different branch and git rmed the extraneous files. There are only four changed files now

[Pietro Monticone]

Merged.

[Pietro Monticone]

Just reviewed and merged equational#1155 and equational#1156 opened by @Aaron Hill.

[Terence Tao]

Thanks @Aaron Hill for the two PRs!

I am closing in on completing equational#1118, which was significantly more complicated than I anticipated. Part of the reason is due to a lot of subtle collision issues that I did not anticipate when writing the blueprint proof, which required multiple refactoring of the argument in which axioms were modified or introduced. I did find a few minor simplifications to compensate though, and am learning how to use tactics such as all_goals to handle large numbers of case checks in an assembly-line fashion, as well as creating dozens of tiny lemmas. Hopefully will be completely done in a day or two.

While the setup was tedious, I can certainly say that refactoring a lengthy and convoluted proof is much nicer to do in a formalized setting than with pen and paper. Making a fundamental change in the axioms and seeing within a minute the dozen or so precise lines of code that need to be changed is very pleasant compared to manual line-by-line verification!

[Terence Tao]

OK, I have an embarrasingly simple request. How does one prove

lemma one_odd (n : ZMod 4) : 1 ≠ n + n := by
  sorry

? I thought this would be a decide but I guess decide does not know how to enumerate over ZMod 4 (or Fin 4).

[Edward van de Meent]

if you revert n, decide should work, i think...

[Edward van de Meent]

alternatively, fin_cases n <;> decide is likely to work too

[Terence Tao]

Ah! that worked. OK, good to know that decide can handle bounded quantifiers if one reverts first.

[Johan Commelin]

Minor QoL improvement: decide +revert

[Terence Tao]

Is this a recent modification to decide? It doesn't seem to work on my build.

[Johan Commelin]

It's been around for a while. This project is on a pretty recent version of Lean, right?

[Shreyas Srinivas]

It is likely. The format for tactic configurations used to be different.

[Shreyas Srinivas]

We haven’t updated the toolchains for a while because one of the update PRs had an unresolved discussion about some upgrade issue.

[Shreyas Srinivas]

Cc: @Pietro Monticone

[Shreyas Srinivas]

We are still at 4.14.0-rc3

[Pietro Monticone]

Yes, there are some remaining non-trivial issues to solve. equational#970

[Pietro Monticone]

Unfortunately I’m very busy at the moment so any help is appreciated

[Shreyas Srinivas]

I think we should hold off until all existing PRs are resolved.

[Shreyas Srinivas]

The following should work on earlier toolchains as well as current ones:

import Mathlib

lemma one_odd (n : ZMod 4) : 1 ≠ n + n := by
  decide (config := {revert := true})

[Kevin Buzzard]

I think that you should aggressively bump mathlib always and rotten luck to the PRs which break. That's been my attitude with FLT. We bump weekly.

[Kevin Buzzard]

Basically the longer you leave it the more the errors pile up. Lean itself is not backwards compatible so after a while the entire config setup fails and you're left trying to solve problems which everyone else solved months ago. When things break with FLT after a bump there are always several other people on the Zulip saying "my project just broke" and explanations of how to fix them. Even the fixes might break if you leave it too long.

[Shreyas Srinivas]

So normally I would agree but Pietro points out there are some breakages that need fixing in the lawful magma proofs. Pietro has said he will look into it.

About your second point : the project will always compile on the current toolchain

[Shreyas Srinivas]

That is to say the toolchain on which the project is currently being built.

[Shreyas Srinivas]

If someone wishes to make a PR to update the toolchain to 4.19.0-rc2 this is most welcome

[Shreyas Srinivas]

If it remains undone I will probably do it later this week.

[Terence Tao]

Finally finished the proof of equational#1118! It was significantly harder than expected. There was one map L₀' which at one point basically was a piecewise defined function with ten pieces, and to verify noncollisions required about a hundred separate verifications, many of whom were broadly similar but with key parameters changed. I finally figured out a way to do all of them in a somewhat civilized way through liberal use of all_goals and simp with a large number of very small lemmas.

At several points in the process, I found that of the 100 or so noncollision statements to check, one or two actually could not be verified from the axioms I was using for a partial solution. So I had to go back and tweak one of the axioms to fix this, which of course broke other things, but thanks to the magic of Lean (and eventually myself realizing to avoid hardcoding various things into the lean proofs), in many cases only a relatively small number of lines of code needed to be changed for each such refactor. It is interesting that a complex proof in Lean feels a lot less "brittle" than a corresponding pen-and-paper proof; past a certain point, I become afraid to tinker with any foundational detail of the latter, but with Lean one can much more confidently tweak the proof in one direction or another.

A final stumbling block was to show that certain expressions in the free group N were not equal to each other. A typical thing to show as that $e_a x = e_0^n e_a y$ was only possible when $n=0$, assuming that $a$ is non-zero and the generator $e_a$ does not appear in the expansions of $x$ or $y$. This looked tricky to do from the direct definition of a free group using reduced words, but I eventually figured out how to use enough of the representation theory API to construct a simple representation of the free group as two-dimensional linear transformations to rule out this sort of identity. (For 90% of the identities needed, one could abelianize and basically count things like how often a given generator like $e_a$ appeared on the left-hand side or right-hand side, but the above was one of the few cases where one could not proceed purely through abelian arguments and had to deploy some actual non-abelian representation, of which the simplest examples came from two dimensions.)

Now I think the only sorry remaining in the entire project is reduce_to_new_axioms. @Shreyas Srinivas , are you still planning to close that one off? If not, I can have a go at it instead.

[Johan Commelin]

Congratulations! That sounds like a Herculean sprint to the finish line!

[Shreyas Srinivas]

I’ll work on the remaining sorries later today

[Shreyas Srinivas]

Johan Commelin said:

Congratulations! That sounds like a Herculean sprint to the finish line!

In a way it was like a relay race and a triathlon.

[Shreyas Srinivas]

Got rid of some sorries in the SmallMagma file.

[Shreyas Srinivas]

More to follow tomorrow.

[Shreyas Srinivas]

@Pietro Monticone : Yesterday's PR basically overrode all the fixes I made

[Shreyas Srinivas]

I'll recover and redo it, but we should come up with a way to avoid this (point to note for the paper)

[Shreyas Srinivas]

I think we are free of sorries now. Just waiting on CI

[Shreyas Srinivas]

Update : CI passes. We are free of sorries

[Notification Bot]

7 messages were moved from this topic to #Equational > Project language stats by Shreyas Srinivas.