olympiad problems with mathlib4

Stream: mathlib4

[David Renshaw]

I think we're at the point where we can try some simple olympiad problems with mathlib4, so I'm going to try that right now on stream: https://www.twitch.tv/dwrensha

[Eric Wieser]

Can mathport not translate this stuff for you?

[David Renshaw]

yeah, but that's less fun

[Jason Rute]

But can LeanAid (#lean4 > LeanAide translation: Natural language to Lean 4) translate it for you. That sounds fun!

[David Renshaw]

First problem: done!
https://github.com/dwrensha/math-puzzles-in-lean4/blob/5e87d4a793f9ec04846b63bdbbdd4ebe5c73f949/MathPuzzles/russia1998_q42.lean

[David Renshaw]

I at first had

variable (R : Type) [CommRing R] [NeZero (2:R)] [CancelMonoidWithZero R]

and that didn't work due to an error

application type mismatch
  Iff.mp (mul_right_inj' ?m.7061) h2
argument
  h2
has type
  @HMul.hMul R R R (@instHMul R NonUnitalNonAssocRing.toMul) 2 x = 2 * a : Prop
but is expected to have type
  @HMul.hMul R R R (@instHMul R MulZeroClass.toMul) 2 x = 2 * a : Prop

[David Renshaw]

but then when I did

class RealLike (R : Type) extends
  CommRing R, NeZero (2:R), CancelMonoidWithZero R

variable (R : Type) [CommRing R] [NeZero (2:R)] [CancelMonoidWithZero R]

it worked.

[David Renshaw]

(I don't think this is a Lean 3 / Lean 4 difference, just something that I stumbled on when trying to mock out the real numbers)

[David Renshaw]

Tonight I'm going to try formalizing some MiniF2F problems with Mathlib4. https://www.twitch.tv/dwrensha

[Heather Macbeth]

Good luck! But I imagine mathlib4#1102 and mathlib4#1189 will be major obstacles ...

[David Renshaw]

yeah, I'm probably going to mostly stick to ints and nats

[David Renshaw]

We found a bug in one of the problems! https://github.com/openai/miniF2F/issues/125

[Eric Wieser]

miniF2F has many such problems, there was a thread about that elsewhere. Facebook's version fixes a small fraction of those.

[David Renshaw]

fwiw, this particular bug is not fixed on the Facebook fork: https://github.com/facebookresearch/miniF2F/blob/5271ddec788677c815cf818a06f368ef6498a106/lean/src/valid.lean#L57-L66

[David Renshaw]

Last night on twitch, I formalized another IMO problem with mathlib4, and today I cut the recording of the 2-hour session into a fast(er) paced 11-minute video: https://youtu.be/9d2nicgd68Q

[David Renshaw]

One interesting outcome was that I ran into this bug: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/weird.20interaction.20between.20.60mod_cases.60.20and.20.60induction.60/near/323603044

[Johan Commelin]

Thanks! I enjoyed watching the video.

[Sebastian Ullrich]

Very nice. Would the obtain \<n, h\> := ...; cases n pattern be covered by cases h : n?

[Sebastian Ullrich]

(The obtain by itself should be docs4#Lean.Parser.Tactic.generalize)

[David Renshaw]

Sebastian Ullrich said:

Very nice. Would the obtain \<n, h\> := ...; cases n pattern be covered by cases h : n?

Yep, thanks! I was hoping someone might teach me the right way to do that.

[Anand Rao]

I enjoyed watching the video. With a slight rephrasing of the problem statement, I managed to golf the proof down to four lines. (I wonder if the n + 3 case can be golfed further to a single line using aesop?)

import Mathlib.Data.Nat.Basic
import Mathlib.Algebra.GroupPower.Basic

theorem imo_1964_q1b : ∀ (n : ℕ), (2 ^ n + 1) % 7 ≠ 0
    | 0 | 1 | 2 => by decide
    | n + 3 => by
      rw [pow_add, Nat.add_mod, Nat.mul_mod, show 2 ^ 3 % 7 = 1 from by rfl]
      simp [imo_1964_q1b n]

[Jannis Limperg]

Probably not; Aesop is no better at equations than simp. You can golf it by putting a semicolon between rw and simp. ;)

[Kevin Buzzard]

This is the canonical easy IMO problem :-) Even the AIs can solve tuff one! Although they take far more lines to do so :-)

[David Renshaw]

Anand Rao said:

I enjoyed watching the video. With a slight rephrasing of the problem statement, I managed to golf the proof down to four lines.

Cool! Care to submit a pull request? https://github.com/dwrensha/math-puzzles-in-lean4

[Siddhartha Gadgil]

@Jannis Limperg Since we are on this topic, @Anand Rao and I were discussing this: how do we add rw [blah] as a tactic in an Aesop call/rule-set?

[Anand Rao]

David Renshaw said:

Anand Rao said:

I enjoyed watching the video. With a slight rephrasing of the problem statement, I managed to golf the proof down to four lines.

Cool! Care to submit a pull request? https://github.com/dwrensha/math-puzzles-in-lean4

Done: https://github.com/dwrensha/math-puzzles-in-lean4/pull/1.

[Jannis Limperg]

Siddhartha Gadgil said:

Jannis Limperg Since we are on this topic, Anand Rao and I were discussing this: how do we add rw [blah] as a tactic in an Aesop call/rule-set?

If you don't want the rewrite to be a simp rule, this is currently the only way:

open Lean.Elab.Tactic in
@[aesop safe]
def myTactic : TacticM Unit := do
  evalTactic $ ← `(tactic| rw [blah])

Admittedly not great. I'll try to come up with a better syntax for adding tactics.

[Siddhartha Gadgil]

Jannis Limperg said:

Siddhartha Gadgil said:

Jannis Limperg Since we are on this topic, Anand Rao and I were discussing this: how do we add rw [blah] as a tactic in an Aesop call/rule-set?

If you don't want the rewrite to be a simp rule, this is currently the only way:

open Lean.Elab.Tactic in
@[aesop safe]
def myTactic : TacticM Unit := do
  evalTactic $ ← `(tactic| rw [blah])

Admittedly not great. I'll try to come up with a better syntax for adding tactics.

Thanks. So I take it for now it should be a single named tactic, not one with parameters.

[Jannis Limperg]

The rw [blah] from my example works if blah is a defined constant. It could also work for hypotheses if Aesop had some syntax to support it. If you mean adding just rw and letting it figure out that it should rewrite with each hypothesis or something along those lines, that's probably not going to be supported.

[Siddhartha Gadgil]

Our goal is to call Aesop programmatically with a bunch of rules, some of which are specific instances of rw. So an API is fine

[Siddhartha Gadgil]

Essentially do a search with Aesop with a large number of rules which the indexing makes cheap and a small number of more carefully chosen tactics, mainly insurances of rw with specified parameters

[Jannis Limperg]

In that case you probably want to be going through the MetaM-level API. The entrypoint is search and you'd want to pass a custom rule set. There's not much documentation (and not much thought has gone into this use case) but I'll be happy to help.

[David Renshaw]

This week I formalized IMO 1964 Q4, a combinatorics problem: https://www.youtube.com/watch?v=TOzS4aC_K1g

[Kevin Buzzard]

Are you doing these things at a regular weekly time?

[David Renshaw]

I've been doing ~7pm Pittsburgh local time on Tuesdays.

[David Renshaw]

Admittedly not a very Europe-friendly time.