McCune's axiom

Stream: maths

[Patrick Massot]

I'm typing lecture notes on basic algebra and I wanted to warn my readers that going too far with axiom optimization can lead to madness. I'm trying to quote one example of a single-axiom definition of groups, and I wanted to see whether there was anyway to write a proof there (I do have some masochistic students). Most papers on this topic seem to simply quote some dead specialized software, but this paper has something that claims to be a proof on Page 10. Is anyone able to decipher that page? This should be pretty easy to formalize if it is true (we could even have that in the archive folder of mathlib).

[Kevin Buzzard]

that looks like a fun project but I bet that the easiest way to do it is to actually fire up some of that ATP software and let it do it itself.

[Patrick Massot]

All this stuff was found by an ATP... which then bit-rot. And all those papers replace most proofs with "the reader should fire up our ATP".

[Kevin Buzzard]

import tactic

variables (G : Type)

example [group G] (x y z u : G) :
  x * (y * (((z * z⁻¹) * (u * y)⁻¹ * x))⁻¹) = u :=
  by group -- fails

I failed to do the easy way :-)

[Kevin Buzzard]

There are about 10 rewrite lemmas due to Knuth and Bendix which are supposed to solve that problem, right?

[Patrick Massot]

Hey, this is not meant to fail.

[Kevin Buzzard]

then maybe I made a typo

[Kevin Buzzard]

I did!

[Patrick Massot]

I did it on paper.

[Kevin Buzzard]

import tactic

variables (G : Type)

example [group G] (x y z u : G) :
  (x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹) = u :=
  by group

[Kevin Buzzard]

the other direction is left as an exercise

[Patrick Massot]

Indeed that's not the correct relation

[Patrick Massot]

import tactic

variables (G : Type)

example [group G] (x y z u : G) :
  x * (y * (((z * z⁻¹) * (u * y)⁻¹ * x)))⁻¹ = u :=
  by group -- works!

[Patrick Massot]

I'm late but my super crappy internet connection is showing me messages late.

[Kevin Buzzard]

import tactic

variables (G : Type)

example [group G] (x y z u : G) :
  (x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹) = u :=
  by group

example [has_mul G] [has_inv G] (h : ∀ x y z u : G, (x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹) = u ) :
  group G := sorry

[Mario Carneiro]

Here's a setup. I failed on the first paramodulation step:

import algebra.group.basic
noncomputable theory

class mccune_group (α : Type*) extends has_mul α, has_inv α :=
(nonemp : nonempty α)
(mccune (x y z u : α) : x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹ = u)

namespace mccune_group
variables {α : Type*} [mccune_group α] (x y z u w v : α)
lemma l5 : x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹ = u := mccune _ _ _ _
lemma l7 : x * ((((y * y⁻¹) * (z * u)⁻¹) * (v * v⁻¹)) * (z * x))⁻¹ = u :=
begin
  have := l5 x y z u,
  have := l5 (v * v⁻¹) u y z,
  -- ???
  sorry
end

instance : has_one α := ⟨let x := classical.choice (@nonemp α _) in x * x⁻¹⟩
lemma mul_assoc : (x * y) * z = x * (y * z) := sorry
lemma one_mul : 1 * x = x := sorry
lemma mul_one : x * 1 = x := sorry
lemma mul_left_inv : x⁻¹ * x = 1 := sorry

instance : group α :=
{ mul := (*), mul_assoc := mul_assoc,
  one := 1, one_mul := one_mul, mul_one := mul_one,
  inv := has_inv.inv, mul_left_inv := mul_left_inv }

[Patrick Massot]

Beware I think the other direction has an implicit assumption that $G$ is not empty.

[Kevin Buzzard]

for sure!

[Eric Rodriguez]

i thought all G had to have a 1

[Eric Rodriguez]

didn't know the rng debate went past ring theory

[Kevin Buzzard]

all groups have a 1, but we're trying to prove something is a group

[Patrick Massot]

And letting the other direction as an exercise is what I intend to do, but I'd like to have the answer somewhere.

[Patrick Massot]

Eric, one of the steps in the proof is meant to be that $\forall x y, xx^{-1} = yy^{-1}$ and then, assuming $G$ is not empty, this common value is defined to be $1$.

[Kevin Buzzard]

@Mario Carneiro if only we could see 6!

[Mario Carneiro]

The proof says that 7 is obtained by paramodulation of 5 into 5. I challenge folks to figure out what that means

[Kevin Buzzard]

I decided it meant substitution of 5 into 5

[Patrick Massot]

Yes, this is where I arrived and got stuck.

[Kevin Buzzard]

Perhaps the author knew that any sane person would have stopped reading by this line so he could write what he liked

[Mario Carneiro]

If you have \all x, l x = r x and \all y, P y, then paramodulation of the first into the second should mean instantiating both to l a = r a and P b, such that l a is a subterm of P b, i.e. P b = Q (l a), resulting in the theorem Q (r a). The non obvious parts are what a, b and Q should be chosen to be such that Q (r a) is the theorem you want

[Kevin Buzzard]

(5) has 7 variables on the LHS, and (7) has 9, but there's no way you can rewrite 5 into itself to make the number of variables only go up by 2

[Kevin Buzzard]

oh I see, you can first make the number go up by 8 and then down by 6

[Kevin Buzzard]

and the "up by 8" equation is missing line 6

[Mario Carneiro]

Yeah when I first heard of the McCune theorem I thought that the first few steps must be gigantic because nothing cancels for a while

[Patrick Massot]

I can feel I only need to wait a little longer and Mario and Kevin will do it for me. I love this place.

[Kevin Buzzard]

I hope it gets easier than this first line!

[Mario Carneiro]

maybe we will need OTTER's help after all

[Mario Carneiro]

plot twist: OTTER was buggy and no one noticed

[Patrick Massot]

Good luck resurrecting OTTER. I think you'll do it faster by hand + Lean.

[Eric Rodriguez]

Mario, I'm taking it that here that our ∀ y, P y is rfl?

[Kevin Buzzard]

surely we can just ask prover9 to do this

[Patrick Massot]

Good luck resurrecting prover9 then.

[Kevin Buzzard]

this is also dead?? These guys must use something?

[Patrick Massot]

It was last updated in 2009, and it doesn't run here, even on a computer that still has python2 installed.

[Patrick Massot]

Maybe McCune died, or he got bored with this kind of research.

[Mario Carneiro]

Eric Rodriguez said:

Mario, I'm taking it that here that our ∀ y, P y is rfl?

No, \all x, l x = r x and \all y, P y are two previously proven steps, specified as inputs. In the case of step 7 it is using step 5 for both

[Mario Carneiro]

P y is an equality too, you are substituting into both sides of it (but the fact it's an equality doesn't matter much since you are only doing equalish stuff for the other lemma)

[Kevin Buzzard]

There is a chance that step 6 has length 100, right?

[Mario Carneiro]

I think step 6 turned out not to be useful

[Mario Carneiro]

the numbering is gapped because the theorem was cleaned up after the fact

[Kevin Buzzard]

...
gcc  -O -Wall -lm -o prover9 prover9.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a
/usr/bin/ld: search.o: in function `search':
search.c:(.text+0x6745): undefined reference to `round'
collect2: error: ld returned 1 exit status
make[1]: *** [Makefile:66: prover9] Error 1
make[1]: Leaving directory '/home/buzzard/Downloads/crap/LADR-2009-11A/provers.src'
make: *** [Makefile:7: all] Error 2
buzzard@bob:~/Downloads/crap/LADR-2009-11A$

Any ideas?

[Patrick Massot]

My bet is on Mario finishing the proof before Kevin can compile that stuff.

[Kevin Buzzard]

prover9.png

[Kevin Buzzard]

now how does it work?

[Kevin Buzzard]

Patrick your mistake was not using Ubuntu, with its built in python2

[Eric Rodriguez]

image.png

[Patrick Massot]

Mario, I'm very disappointed.

[Kevin Buzzard]

How long is it supposed to take to find this two-line proof?

[Eric Rodriguez]

can't be that slow on modern computers

[Patrick Massot]

The paper spends a lot of pages explaining how to tweak the parameters of the previous software.

[Eric Rodriguez]

image.png

I am way too young

[Kevin Buzzard]

do you know what a megabyte is? We used to have them in the old days

[Patrick Massot]

I used to have a 486 computer :older_man:

[Eric Rodriguez]

is it that "MB" thing that leanproject get-cache is on about ;b

[Kevin Buzzard]

I used to have a 6502 computer :P

[Eric Rodriguez]

BBC Micro? My ICT professor loved those things, he taught us programming in its BASIC dialect actually

[Eric Rodriguez]

he brought one in one day and I blew one of the caps on it...

[Kevin Buzzard]

The one before -- an Acorn Atom, with a more primitive BASIC. Back to the point, prover9 is supposed to be giving up after 60 seconds but it's just sitting there pulsating and failing to solve the goal

[Patrick Massot]

I wonder whether McCune originally included all steps and then the journal editor asked for a shorten version.

[Mario Carneiro]

Patrick Massot said:

Mario, I'm very disappointed.

Don't count your chickens before they hatch; I haven't seen a proof of l7 yet

[Kevin Buzzard]

"remove 50% of steps because all arguments here are clearly trivial"

[Patrick Massot]

Maybe there was a page number limit from the beginning, as in computer science proceedings.

[Kevin Buzzard]

1 x * ((((y * y') * (z * u)') * (w * w')) * (z * x))' = u # label(non_clause) # label(goal).  [goal].
2 x * (y * (((z * z') * (u * y)') * x))' = u.  [assumption].
3 c1 * ((((c2 * c2') * (c3 * c4)') * (c5 * c5')) * (c3 * c1))' != c4.  [deny(1)].
5 x * ((((y * y') * (z * u)') * (w * w')) * (z * x))' = u.  [para(2(a,1),2(a,1,2,1,2,1))].
6 $F.  [resolve(5,a,3,a)].

[Kevin Buzzard]

My mistake was that I used \-1 for inverse, and the terminal was full of "hey this is not ASCII!" errors

[Kevin Buzzard]

lol does this help?

[Eric Rodriguez]

I also got some length otter output: https://gist.github.com/ericrbg/199c0679656f7a394b42dc0cf6a11fe4

[Kevin Buzzard]

I think the only new information is that the hint 5 -> 5 has been expanded to para(2(a,1),2(a,1,2,1,2,1))

[Kevin Buzzard]

well Eric's answer is certainly more information

[Kevin Buzzard]

half of me is wondering whether these so-called "provers" just print out junk randomly, on the basis that humans are never going to actually check this stuff

[Eric Rodriguez]

yeah I have absolutely no clue what it did if I'm honest

[Kevin Buzzard]

https://www.karlin.mff.cuni.cz/~stanovsk/math/bruck_wm.pdf is my favourite computer proof

[Eric Rodriguez]

half of the time I spent was turning the damn thing out of infix to prefix form

[Eric Rodriguez]

Kevin Buzzard said:

https://www.karlin.mff.cuni.cz/~stanovsk/math/bruck_wm.pdf is my favourite computer proof

what is that trying to prove?!

[Kevin Buzzard]

Every Bruck loop with abelian inner mapping group has nilpotency class at most 2. The actual statement being proved is on the first page of the 1000 page pdf

[Eric Wieser]

Eric Rodriguez said:

half of the time I spent was turning the damn thing out of infix to prefix form

notation `f(`x`,`y`)` := id (x * y)
notation `h(`x`)` := id (x⁻¹)

helps with that

[Eric Wieser]

Then you can use dsimp to throw away the awful notation

[Kevin Buzzard]

From the manual: "para(47(a,1),28(a,1,2,2,1)) -- paramodulate from the clause 47 into clause 28 at the positions shown. "

[Bhavik Mehta]

import tactic

class mccune_group (α : Type*) extends has_mul α, has_inv α :=
(mccune (x y z u : α) : x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹ = u)

namespace mccune_group
variables {α : Type*} [mccune_group α] (x y z u w v : α)

lemma l5 : x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹ = u := mccune _ _ _ _

lemma l7 : x * ((((y * y⁻¹) * (z * u)⁻¹) * (v * v⁻¹)) * (z * x))⁻¹ = u :=
begin
  set q := ((y * y⁻¹) * (z * u)⁻¹) * (v * v⁻¹),
  rw ←l5 (v * v⁻¹) u y z,
  rw l5 x q v u,
end

end mccune_group

I haven't followed this thread but here's the first line

[Kevin Buzzard]

Discord FTW

[Bhavik Mehta]

Exactly as claimed, it is just paramodulation

[Eric Wieser]

Why does it fail without the set line?

[Kevin Buzzard]

I got it first, the proof is just para(2(a,1),2(a,1,2,1,2,1))

[Eric Wieser]

(deleted)

[Bhavik Mehta]

Eric Wieser said:

Why does it fail without the set line?

I'm sure it's possible without that, with some more targeted rewrites, but it does the job :)

[Kevin Buzzard]

Next level:

lemma l9 : (x * ((y * (z * z⁻¹)) * (u * x))⁻¹) = (((v * v⁻¹) *(y * u)⁻¹) * (w * w⁻¹)) :=
begin
  sorry
end

[Kevin Buzzard]

hint: use l5 and l7

[Eric Wieser]

A shorter version of l7 requiring less intuition:

lemma l7 : x * ((((y * y⁻¹) * (z * u)⁻¹) * (v * v⁻¹)) * (z * x))⁻¹ = u :=
begin
  convert l5 _ _ _ _,
  rw l5,
end

[Kevin Buzzard]

I had been trying with convert before I decided to go for the prover9 option (it was on my job list to play around with an ATP at some point in my life)

[Eric Wieser]

lemma l9 : (x * ((y * (z * z⁻¹)) * (u * x))⁻¹) = (((v * v⁻¹) *(y * u)⁻¹) * (w * w⁻¹)) :=
begin
  convert l7 _ _ _ _ _,
  rw l5,
end

[Bhavik Mehta]

You beat me to it by a second, Eric! :grinning:

[Eric Wieser]

So A -> B means convert B, rw A?

[Eric Rodriguez]

Kevin Buzzard said:

hint: use l5 and l7

this is most textbook hints summed up

[Bhavik Mehta]

I think a more faithful translation might be rewrite with the inverse of A at a specific place so that B applies

[Bhavik Mehta]

But pragmatically it seems like convert, rw does the trick

[Eric Wieser]

If my claim is true this should get us all the way to l15, and then we have to know what : means

[Bhavik Mehta]

: supposedly means simplify using that axiom

[Kevin Buzzard]

lemma l10 : (((y * y⁻¹)*(((z*z⁻¹)*(u*x)⁻¹)*u)⁻¹)*(v*v⁻¹))=x :=
begin
  sorry
end

[Kevin Buzzard]

hint: 7 -> 9

[Eric Wieser]

Damn

[Bhavik Mehta]

Eric's magic incantation doesn't do it :(

[Eric Wieser]

lemma l10 : (((y * y⁻¹)*(((z*z⁻¹)*(u*x)⁻¹)*u)⁻¹)*(v*v⁻¹))=x :=
begin
  rw ←l9,
  apply l7,
  exact x,
  exact z,
end

[Eric Wieser]

I don't know where those exacts came from, since it seems they have no requirements?

[Yaël Dillies]

What does refine spit out?

[Eric Rodriguez]

lemma l12 : (((x * x⁻¹)*y⁻¹⁻¹)*(z*z⁻¹))=y :=
begin
  convert l10,
  rw l10,
  exact x
end

[Bhavik Mehta]

Hmm that doesn't seem to work for me...

[Kevin Buzzard]

I think Eric R must have implicit variables

[Bhavik Mehta]

lemma l14 : ((x*x⁻¹)*(y*z)⁻¹)=((u*u⁻¹)*(y*z)⁻¹) := -- [10 -> 5]
begin
  convert l5 _ _ _ _,
  rw l10,
  exact x,
end

[Eric Rodriguez]

oh I made implicits everywhere so just stick some _ s

[Kevin Buzzard]

Eric we're live streaming on the discord

[Bhavik Mehta]

lemma l15 : ((x*x⁻¹)*y⁻¹) = ((z*z⁻¹)*y⁻¹) := -- [12 -> 14 : 12]
begin
  convert l14 _ _ _ _,
  rw l12,
  exact x,
  exact z,
  rw l12,
end

[Eric Wieser]

Do any of these exacts matter?

[Bhavik Mehta]

Their values don't, but they are important

[Bhavik Mehta]

In l15 after the first line it just wants that y is a product of two things

[Bhavik Mehta]

and here l12 says that it is, and it doesn't matter what the two things are; they just need to be given

[Patrick Massot]

I love that creative use of convert.

[Kevin Buzzard]

Yes, it reminded me of that comment that Lean was supposed to be bridging the gap between ATP and ITP

[Patrick Massot]

Of course we know that unification is a huge crucial piece of the puzzle. But we're not used it seeing it used in such a spectacular way.

[Patrick Massot]

Let me ping @Simon Hudon who wrote convert (at least the original implementation, see this thread).

[Bhavik Mehta]

lemma l17 : u * u⁻¹ = v * v⁻¹ := -- [15 → 5 : 5]
begin
  rw ←l5 u u⁻¹ u (v * v⁻¹),
  rw l15 v _,
  rw l5,
end

[Bhavik Mehta]

lemma l19 : x * x⁻¹ = ((y * y⁻¹) * (z * z⁻¹)⁻¹) := -- [17 → 15]
begin
  rw [l15],
  exact l17 _ _,
end

I'll stop with the constant updates, but I'm working on this in the discord with Kevin

[Eric Wieser]

How many lines are there total?

[Bhavik Mehta]

Getting past 100, but I'm also adding notations and simp lemmas to make the proofs easier

[Eric Wieser]

(I mean in the LaTeX proof not lines of lean code, to be clear)

[Eric Rodriguez]

is the plan to PR this to mathlib?

[Eric Wieser]

It probably would be nice in archive if it doesn't make it to src

[Eric Wieser]

(oh, I see Patrick already suggested archive at the start of the thread)

[Simon Hudon]

@Patrick Massot thanks for pinging me! It is indeed a pretty cool use of convert. I wonder if we could avoid all those superfluous _. We could make it more like apply and just automatically insert all the _ it will take

[Eric Wieser]

Yes, my main criticism of convert is that if you don't give enough arguments you get a nonsense goal state that doesn't even typecheck like a + b = b + a = ∀ c, c + b = b + a

[Bhavik Mehta]

Well technically it does typecheck, they're both Props

[Eric Wieser]

Ah you're right, the case I'm thinking of has another =

[Kevin Buzzard]

import tactic

class mccune_group (α : Type*) extends has_mul α, has_inv α :=
(mccune (x y z u : α) : x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹ = u)

namespace mccune_group
variables {α : Type*} [mccune_group α] (x y z u w v : α)

lemma l5 : x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹ = u := mccune _ _ _ _

lemma l7 : x * ((((y * y⁻¹) * (z * u)⁻¹) * (v * v⁻¹)) * (z * x))⁻¹ = u :=
begin
  convert l5 _ _ _ _,
  rw l5,
end

lemma l9 : (x * ((y * (z * z⁻¹)) * (u * x))⁻¹) = (((v * v⁻¹) *(y * u)⁻¹) * (w * w⁻¹)) :=
begin
  convert l7 _ _ _ _ _,
  rw l5,
end

lemma l10 : (((y * y⁻¹)*(((z*z⁻¹)*(u*x)⁻¹)*u)⁻¹)*(v*v⁻¹))=x :=
begin
  rw ←l9,
  apply l7,
  exact x, exact x,
end

lemma l12 : (((x*x⁻¹)*y⁻¹⁻¹)*(z*z⁻¹)) = y := -- [10 -> 10]
begin
  convert l10 _ _ _ _ _,
  rw l10,
  exact x
end

lemma l14 : ((x*x⁻¹)*(y*z)⁻¹)=((u*u⁻¹)*(y*z)⁻¹) := -- [10 -> 5]
begin
    convert l5 _ _ _ _,
  rw l10,
  exact x,
end

lemma l15 : ((x*x⁻¹)*y⁻¹) = ((z*z⁻¹)*y⁻¹) := -- [12 -> 14 : 12]
begin
    convert l14 _ _ _ _,
  rw l12,
  exact x,
  exact z,
  rw l12,
end

lemma l17 : u * u⁻¹ = v * v⁻¹ := -- [15 → 5 : 5]
begin
  rw ←l5 u u⁻¹ u (v * v⁻¹),
  rw l15 v _,
  rw l5,
end

lemma l19 : x * x⁻¹ = ((y * y⁻¹) * (z * z⁻¹)⁻¹) := -- [17 → 15]
begin
  rw [l15],
  exact l17 _ _,
end

lemma l20 : (((x * x⁻¹) * ((y * y⁻¹)*z)⁻¹)*(u*u⁻¹)) = z⁻¹ := -- [17 → 10]
begin
  sorry
end

lemma l22 : (x * (y⁻¹ * ((z*z⁻¹)*x))⁻¹) = y := -- [17 → 5]
begin
  sorry
end

lemma l25 : (x*((u*u⁻¹)⁻¹⁻¹*(w*x))⁻¹)=w⁻¹ := -- [19 → 7:20]
sorry

lemma l32 : ((x*x⁻¹)⁻¹*(y⁻¹*(z*z⁻¹))⁻¹) = y := -- [17 → 22]
sorry

lemma l34 : (x⁻¹*((y*y⁻¹)⁻¹⁻¹*(z*z⁻¹))⁻¹)=x⁻¹ := -- [17->25]
sorry

lemma l36 : ((y*y⁻¹)*(x*(z*z⁻¹)⁻¹⁻¹)⁻¹)⁻¹=x := -- [5->25]
sorry

lemma l44 : (x*((y*y⁻¹)⁻¹⁻¹*(z*z⁻¹))⁻¹)=x := -- [36 ->34:36]
sorry

lemma l48 : ((x*x⁻¹)⁻¹⁻¹*(y*y⁻¹))=(z*z⁻¹) := -- [44->17]
sorry

lemma l52 : (x*(y*y⁻¹)⁻¹)=x := -- [52->10:20]
sorry

lemma l57 : ((z*z⁻¹)⁻¹*u)⁻¹⁻¹=u := -- [52->10:20]
sorry

lemma l62 : (x⁻¹*(y*y⁻¹))⁻¹=x⁻¹⁻¹ := --[32->57]
sorry

lemma l65 : (y*((z*z⁻¹)*(x*y)⁻¹))⁻¹=x⁻¹⁻¹ := --[5->57:52]
sorry

lemma l76 : (x*(y*y⁻¹))⁻¹=x⁻¹ := -- [57->62:57]
sorry

lemma l88 : ((x*x⁻¹)⁻¹*y⁻¹⁻¹)=y := -- [65->32]
sorry

lemma l92 : ((u*u⁻¹)*y⁻¹)⁻¹=y := -- [65->20:12,76]
sorry

lemma l116 : (y*(u*u⁻¹))=y := -- 76-32:76,88
sorry

lemma l126 : ((y*z)*z⁻¹)=y := -- 76->5:92
sorry

lemma l201 : (x*y⁻¹⁻¹)=(x*y) := -- 126 -> 126
sorry

lemma l207 : ((x*x⁻¹)*z)=z := -- 19 -> 126:52,201
sorry

lemma l215 : (x*(y*((x*y)⁻¹*u)))=u := -- 5->126:207,201
sorry

lemma l227 : y⁻¹⁻¹ = y := -- [126->36:207,52]
sorry

lemma l229 : (z*x)⁻¹=x⁻¹*z⁻¹ := -- 126->25:227,207
sorry

lemma l239 : (x*((x⁻¹*u)*y))=u*y := -- [126->5:207,229,229,227,227]
sorry

lemma l260 : ((x*y)*z)=(x*(y*z)) := -- [215->215:229,229,229,227,227,239]
sorry

example (α : Type) [h : inhabited α] : group α ≃ mccune_group α :=
{ to_fun := by introI i; exact
  { mul := (*),
    inv := has_inv.inv,
    mccune := by intros; group },
  inv_fun := by introI i; exact
  { mul := (*),
    mul_assoc := l260,
    one := arbitrary α * (arbitrary α)⁻¹,
    one_mul := l207 _,
    mul_one := λ _, l116 _ _,
    npow := sorry,
    npow_zero' := sorry,
    npow_succ' := sorry,
    inv := has_inv.inv,
    div := sorry,
    div_eq_mul_inv := sorry,
    gpow := sorry,
    gpow_zero' := sorry,
    gpow_succ' := sorry,
    gpow_neg' := sorry, -- there should be a constructor which fills in the last 9 sorries
    mul_left_inv := begin sorry end }, -- unfortunately `l17` is mul_right_inv
    left_inv := begin sorry end, -- need "two groups structures on G are equal iff they have the same mul"
    right_inv := begin intro h2, cases h2, simp, sorry end, -- need an ext for mccune_groups
  }

end mccune_group

[Kevin Buzzard]

Bhavik is up to l126

[Mario Carneiro]

Why didn't I need all that junk in the group constructor here?

[Mario Carneiro]

I don't think I'm on a relevantly old mathlib

[Kevin Buzzard]

I just used the bottom but one hole-filler

[Kevin Buzzard]

oh it's because

(gpow : ℤ → G → G := gpow_rec)
(gpow_zero' : ∀ (a : G), gpow 0 a = 1 . try_refl_tac)
(gpow_succ' :
  ∀ (n : ℕ) (a : G), gpow (int.of_nat n.succ) a = a * gpow (int.of_nat n) a  . try_refl_tac)
(gpow_neg' :
  ∀ (n : ℕ) (a : G), gpow (-[1+ n]) a = (gpow n.succ a) ⁻¹ . try_refl_tac)

they all have default values, which "generate a skeleton for the structure under construction" doesn't ignore.

[Mario Carneiro]

you shouldn't need an ext for mccune groups, it's trivial

[Mario Carneiro]

cases, cases, refl should work

[Kevin Buzzard]

Bhavik's code diverges from this too, I think I'll leave it here and he can post his final answer later when he's cracked 126

[Bhavik Mehta]

Pretty mucky:

import tactic

class mccune_group (α : Type*) extends has_mul α, has_inv α, inhabited α :=
(mccune (x y z u : α) : x * (y * (((z * z⁻¹) * (u * y)⁻¹) * x))⁻¹ = u)

namespace mccune_group
variables {α : Type*} [mccune_group α] (x y z u w v : α)

lemma l5 : x * (y * (z * z⁻¹ * (u * y)⁻¹ * x))⁻¹ = u := mccune _ _ _ _

lemma l7 : x * (y * y⁻¹ * (z * u)⁻¹ * (v * v⁻¹) * (z * x))⁻¹ = u :=
by simpa [l5 (v * v⁻¹)] using l5 x (y * y⁻¹ * (z * u)⁻¹ * (v * v⁻¹)) v u

lemma l9 : x * (y * (z * z⁻¹) * (u * x))⁻¹ = v * v⁻¹ * (y * u)⁻¹ * (w * w⁻¹) :=
by simpa [l5 (w * w⁻¹)] using l7 x w u (v * v⁻¹ * (y * u)⁻¹ * (w * w⁻¹)) z

lemma l10 : y * y⁻¹ * (z * z⁻¹ * (u * x)⁻¹ * u)⁻¹ * (v * v⁻¹) = x :=
by simpa [l9 _ _ _ u v y] using l7 x z u x z

lemma l12 : x * x⁻¹ * y⁻¹⁻¹ * (z * z⁻¹) = y :=
by simpa [l10] using l10 y x x (y * y⁻¹ * (y * y⁻¹)⁻¹) z

lemma l14 : (x * x⁻¹) * (y * z)⁻¹ = u * u⁻¹ * (y * z)⁻¹ := -- [10 -> 5]
begin
  convert l5 _ _ _ _,
  rw l10,
  exact x,
end

lemma l15 : (x * x⁻¹) * y⁻¹ = (z * z⁻¹) * y⁻¹ :=
by simpa [l12] using l14 x ((x * x⁻¹) * y⁻¹⁻¹) (z * z⁻¹) z

lemma l17 : u * u⁻¹ = v * v⁻¹ := -- [15 → 5 : 5]
begin
  rw ←l5 u u⁻¹ u (v * v⁻¹),
  rw l15 v _,
  rw l5,
end

instance : has_one α := ⟨default α * (default α)⁻¹⟩

@[simp] lemma l17' : u * u⁻¹ = 1 := l17 _ _

lemma l10' : (1 * ((1 * (u * x)⁻¹) * u)⁻¹) * 1 = x := l10 _ _ _ _ _

lemma l20' : (1 * (1*z)⁻¹)*1 = z⁻¹ :=
begin
  convert l10' _ _,
  rw l17',
  rw l17',
end

lemma l5' : x * (y * ((1 * (u * y)⁻¹) * x))⁻¹ = u := l5 _ _ _ _

lemma l22' : x * (y⁻¹ * (1 * x))⁻¹ = y := -- [17 → 5]
by { convert l5' _ _ y, simp }

lemma l7' : x * (((1 * (z * u)⁻¹) * 1) * (z * x))⁻¹ = u := l7 _ _ _ _ _

lemma l25' : x * (1⁻¹⁻¹ * (w * x))⁻¹ = w⁻¹ := -- [19 → 7:20]
begin
  convert l7' _ _ _,
  rw l17',
  convert (l20' _).symm,
  simp,
end

lemma l32' : 1⁻¹ * (y⁻¹ * 1)⁻¹ = y := -- [17 → 22]
begin
  convert l22' (1 : α)⁻¹ y,
  simp
end

lemma l34' : x⁻¹ * (1⁻¹⁻¹ * 1)⁻¹ = x⁻¹ := by simpa using l25' x⁻¹ x

lemma l36' : (1 * (x * 1⁻¹⁻¹)⁻¹)⁻¹ = x :=
begin
  convert l5' _ _ _,
  rw l25',
  exact x
end

lemma l44' : x * (1⁻¹⁻¹ * 1)⁻¹ = x := by simpa [l36'] using l34' (1 * (x * 1⁻¹⁻¹)⁻¹)
lemma l48' : (1 : α)⁻¹⁻¹ * 1 = 1 := by simpa using (l44' ((1 : α)⁻¹⁻¹ * 1)).symm
lemma l52' : x * 1⁻¹ = x := by simpa [l48'] using l44' x
lemma l57' : (1⁻¹ * u)⁻¹⁻¹ = u := by simpa [l52', l20'] using l10' u 1⁻¹

lemma l62' : (x⁻¹ * 1)⁻¹ = x⁻¹⁻¹ :=
by simpa [l32'] using (l57' (x⁻¹ * 1)⁻¹).symm

lemma l76' : (x * 1)⁻¹ = x⁻¹ := by simpa [l57'] using l62' (1⁻¹ * x)⁻¹

lemma l88' : 1⁻¹ * x⁻¹⁻¹ = x :=
by simpa [l76'] using l32' x

@[simp] lemma l116' : y * 1 = y :=
begin
  have := l88' (y * 1),
  rw l76' at this,
  rw l88' at this,
  exact this.symm
end

@[simp] lemma one_inv_inv : (1 : α)⁻¹⁻¹ = 1 :=
by simpa using l48'

@[simp] lemma one_inv : (1 : α)⁻¹ = 1 :=
by simpa using l88' (1 : α)

lemma l92' : (1 * y⁻¹)⁻¹ = y :=
by simpa using l36' y

lemma l126' : (y * z) * z⁻¹ = y :=
begin
  have := l5' ((1 : α) * (y * z)⁻¹)⁻¹ z y,
  rw l17' at this,
  simpa [l92'] using this,
end

lemma l201 : x * y⁻¹⁻¹ = x * y :=
by simpa [l126' x y] using l126' (x * y) y⁻¹

@[simp] lemma l207' : 1 * z = z :=
by simpa [l201] using l126' z z⁻¹

@[simp] lemma l227 : y⁻¹⁻¹ = y :=
by simpa using l201 1 y

@[simp] lemma inv_mul : x⁻¹ * x = 1 :=
by simpa using l17' x⁻¹

lemma l229 : (z * x)⁻¹ = x⁻¹ * z⁻¹ := -- 126->25:227,207
by simpa [l126'] using (l25' x⁻¹ (z * x)).symm

lemma thingy : x * (x⁻¹ * z) = z := -- [126->5:207,229,229,227,227]
begin
  have := l5' x z⁻¹ z,
  simp only [one_inv, l17', l207'] at this,
  rw [l229, l227] at this,
  exact this,
end

lemma l239 : x * ((x⁻¹ * u) * y) = u * y := -- [126->5:207,229,229,227,227]
by simpa [l229, l126'] using l5' x y⁻¹ (u * y)

lemma l260 : (x * y) * z = x * (y * z) := -- [215->215:229,229,229,227,227,239]
begin
  rw ←l239 x⁻¹ z y,
  rw thingy,
  simp
end

instance : group α :=
{ mul_assoc := l260,
  one_mul := by simp,
  mul_one := by simp,
  mul_left_inv := λ x, inv_mul _,
  ..(by apply_instance : has_one α),
  ..(by apply_instance : has_mul α),
  ..(by apply_instance : has_inv α) }

end mccune_group

[Bhavik Mehta]

For some of the later ones I made new lemmas instead of the ones from the paper because they made more sense to me

[Patrick Massot]

Thank you very much for your patience Bhavik. This stuff is pretty fascinating in its own very weird way.

[Eric Wieser]

Interesting enough for the archive, right?

[Bhavik Mehta]

#8399

[Bhavik Mehta]

For fun I did the abelian version too (theorem 2 from the paper Patrick linked):

class mccune_comm_group (α : Type*) extends has_mul α, has_inv α, inhabited α :=
(mccune (x y z : α) : x * y * z * (x * z)⁻¹ = y)

namespace mccune_comm_group
variables {α : Type*} [mccune_comm_group α] (x y z u v w : α)

lemma l10 : x * y * (z * x * u * y)⁻¹ = (z * u)⁻¹ :=
by simpa [mccune] using mccune (z * x * u) (z * u)⁻¹ y

lemma l12 : x * (y * x * (y * z)⁻¹)⁻¹ = z := by simpa [mccune] using mccune (y * x) z (y * z)⁻¹
lemma l16 : x * (y * z)⁻¹ * x⁻¹ = (y * z)⁻¹ := by simpa [mccune] using l10 x (y * z)⁻¹ y z
lemma l18 : (y * (z * (y * z * x)⁻¹))⁻¹ = x :=
by simpa [l10] using l12 (z * (y * z * x)⁻¹) (y * z) x
lemma l23 : (x * y * (x * (y * z))⁻¹)⁻¹ = z := by simpa [l10] using l18 z (x * y) (y * z)
lemma l37 : x * y * x⁻¹ = y := by simpa [l23] using l16 x (x * x) (x * (x * y))⁻¹
lemma l39 : (z * y * (z * x)⁻¹)⁻¹ = x * y⁻¹ := by simpa [l12] using (l16 y (z * y) (z * x)⁻¹).symm
lemma l41 : x * (y * x * z)⁻¹ = (y * z)⁻¹ := by simpa [mccune] using l16 (y * x * z) y z
lemma l43 : x * (z * x⁻¹) = z := by simpa [l39] using l12 x x z
lemma l51 : (x * (x * z)⁻¹)⁻¹ = z := by simpa [l41] using l18 z x x
lemma l53 : x * (y * x)⁻¹ = y⁻¹ := by simpa [l37] using l37 (y * x) y⁻¹
lemma l55 : (y * z)⁻¹ = y⁻¹ * z⁻¹ := by simpa [l53, l37] using (l10 z (y * z)⁻¹ y z).symm
lemma l58 : x * y * z * x⁻¹ * y⁻¹ = z := by simpa [l37] using mccune (x * y) z x⁻¹
lemma l60 : x * (y⁻¹ * y⁻¹⁻¹) = x := by simpa [l37, l55] using mccune y x y⁻¹
lemma l64 : x⁻¹ * (x⁻¹⁻¹ * y⁻¹⁻¹) = y := by simpa [l55] using l51 x y
@[simp] lemma l85 : x⁻¹⁻¹ = x := by simpa [l43] using l64 x x
lemma l92 : x⁻¹ * (x * y) = y := by simpa using l64 x y
lemma l94 : x * (y⁻¹ * y) = x := by simpa using l60 x y
lemma l101 : x * (x⁻¹ * y) = y := by simpa using l92 x⁻¹ y
lemma l108 : x * y = y * x := by simpa [l92] using l37 y⁻¹ (y * x)
lemma l114 : x * (y * y⁻¹) = x := by simpa using l94 x y⁻¹
lemma l136 : x * x⁻¹ = y * y⁻¹ := by simpa [l114] using l101 x (y * y⁻¹)
lemma l172 : z * x * y * z⁻¹ = x * y := by simpa [l58] using (l43 x (z * x * y * z⁻¹)).symm
lemma l184 : x * y * z = z * x * y := by simpa [l92 z x] using l172 (z * x) y z⁻¹
lemma l244 : x * y * z = x * (y * z) := by simpa [l184 y] using (l108 x (y * z)).symm

/-- Every McCune comm group is a comm group. -/
instance : comm_group α :=
{ mul_assoc := l244,
  one := default α * (default α)⁻¹,
  mul_one := λ x, l114 x _,
  mul_comm := l108,
  mul_left_inv := λ x, (l108 _ x).trans (l136 x (default α)),
  one_mul := λ x, by rw [l108, l114],
  ..(by apply_instance : has_mul α),
  ..(by apply_instance : has_inv α) }

end mccune_comm_group

[Oliver Nash]

I never fully believed these axioms until you did this! Amazing work.

[Kevin Buzzard]

You didn't believe the computer??

[Oliver Nash]

I had my doubts. Perhaps if I’d read the literature, they would have evaporated. (Or not!)

[Bhavik Mehta]

Since I'm on a roll with these, I'm now doing the Robbins conjecture too in the discord

[Mario Carneiro]

If you are taking requests, you should try doing Meredith's axiom and Wolfram's axiom too

[Adam Topaz]

@Mario Carneiro do you know if there is such a minimal axiom for rings?

[Yaël Dillies]

Wanna create archive/minimal_axiom/? :wink:

[Julian Külshammer]

When I started with Lean, I did the much easier independent vector space axioms from https://www.cambridge.org/core/journals/mathematical-gazette/article/abs/independent-axioms-for-vector-spaces/0D49E4127F5F5EBC788A4AF36E95F07E#

[Mario Carneiro]

@Adam Topaz I wouldn't be surprised if there is one out there, but I haven't heard of any

[Patrick Massot]

Oliver Nash said:

I never fully believed these axioms until you did this! Amazing work.

Once you start to think a bit about the proof, the unbelievable part is that any simplification will occur without knowing associativity. Even the first lemma is still a miracle for me (you can see more information using the version of the proof that I posted in the PR review).

[Bhavik Mehta]

def robbins_conjecture {α : Type*} [has_sup α] [has_compl α] [inhabited α]
  [is_commutative α (⊔)] [is_associative α (⊔)]
  (robbins_axiom : ∀ (x y : α), ((x ⊔ y)ᶜ ⊔ (x ⊔ yᶜ)ᶜ)ᶜ = x) :
  boolean_algebra α :=

works! It's about 5x longer than the McCune group and about 10x longer than the McCune abelian group versions (and roughly the same scale of latex proof and time spent)

[Jasmin Blanchette]

Mario Carneiro said:

The proof says that 7 is obtained by paramodulation of 5 into 5. I challenge folks to figure out what that means

This is a paramodulation (or superposition) inference from and to the same clause. E.g. if you have a = b \/ p a, doing such a paramodulation might yield a = b \/ a = b \/ p b.