Basic questions on the formalization of Maths exercises

Stream: general

[Stanislas Polu]

I'm trying to formalize all the AMC 12A 2021 problems and while I decided to skip entirely geometry problems (though this one may be doable I think?), there are two problems on which I'm struggling that may still be formalized but I probably lack the knowledge.

• The first one is problem 5, where we need to formalize a repetitive infinite decimal expansion of the form 1.ababababa.... Any tool available to do so?
• The second one is problem 15 which is a combinatorics problem and I'm not sure what's the current state of affair in mathlib wrt to these statements?

Thank you very much for your help as always!

[Kevin Buzzard]

We have convergent infinite sums e.g. (I'm over-importing here)

import analysis.specific_limits
import data.real.basic

example (n : ℕ) (h : (66 : ℝ) * (1 + n / 100) + 0.5 = 66 * (1 + ∑' j : ℕ, (n * 0.01^(j+1)))) :
  n = 37 -- or whatever
:=
sorry

(and presumably normed_ring.tsum_geometric_of_norm_lt_1 will help to solve it)

[Yaël Dillies]

Problem 15 is definitely doable, but I fear it may be a bit of a pain.
For solution 1, you'll need to be close to a finset virtuose, but the proof will be okay.
For solution 2, we have Vandermonde's identity (thanks Johan!) but no relation between the terms and a size condition.
For solution 3, I know @Bhavik Mehta proved stuff using generating functions (the partition theorem, for anyone interested) but he never had to evaluate anything. Might be tricky but I don't know.
For solution 4, yeah, that works. Not very fun though.

[Kevin Buzzard]

How would you state it Yael?

[Kevin Buzzard]

Presumably the multiple of 4 condition is some Covid restriction? (I guess it could be something to do with arranging the singers on the stage...)

[Kevin Buzzard]

I guess you can look at (T : finset (fin 6)) and (B : finset (fin 8))

[Yaël Dillies]

import data.nat.modeq

example : fintype.card {finset (fin 6) × finset (fin 8) // λ ⟨t, b⟩, t.card ≡ b.card [MOD 4] ∧ 1 ≤ t.card + b.card} = 4095 := sorry

[Yaël Dillies]

Eheh, that was my idea too.

[Kevin Buzzard]

Spoiler alert!

[Stanislas Polu]

Kevin Buzzard said:

We have convergent infinite sums e.g. (I'm over-importing here)

import analysis.specific_limits
import data.real.basic

example (n : ℕ) (h : (66 : ℝ) * (1 + n / 100) + 0.5 = 66 * (1 + ∑' j : ℕ, (n * 0.01^(j+1)))) :
  n = 37 -- or whatever
:=
sorry

(and presumably normed_ring.tsum_geometric_of_norm_lt_1 will help to solve it)

Thanks! Out of curiosity, If I read correctly the definition docstring, it's a sum without the finset restriction st if the sum converges it's the sum itself or the empty set otherwise. How does that translate when you compose it with + ? Does it collapses to 0 if not defined (Not really important here though as we'll know it converges).

[Kevin Buzzard]

Yes, I think all infinite sums are defined to be 0 if they don't converge in actual-math. It's called tsum in mathlib.

[Stanislas Polu]

Yaël Dillies said:

import data.nat.modeq

example : fintype.card {finset (fin 6) × finset (fin 8) // λ t b, t.card ≡ b.card [MOD 4] ∧ 1 ≤ t.card + b.card} = 4095 := sorry

Ouah! I will need to ponder more on that, but this is incredibly useful!! Thanks!

[Eric Wieser]

Yaël Dillies said:

import data.nat.modeq

example : fintype.card {finset (fin 6) × finset (fin 8) // λ t b, t.card ≡ b.card [MOD 4] ∧ 1 ≤ t.card + b.card} = 4095 := sorry

That's a syntax error

[Yaël Dillies]

Fixed already ;)

[Eric Wieser]

Yaël Dillies said:

import data.nat.modeq

example : fintype.card {finset (fin 6) × finset (fin 8) // λ ⟨t, b⟩, t.card ≡ b.card [MOD 4] ∧ 1 ≤ t.card + b.card} = 4095 := sorry

That's also a syntax error

[Sebastien Gouezel]

import analysis.normed_space.basic

set_option profiler true

example :
  fintype.card {p // (p : finset (fin 6) × finset (fin 8)).1.card ≡ p.2.card [MOD 4] ∧ 1 ≤ p.1.card + p.2.card} = 4095 :=
dec_trivial

[Sebastien Gouezel]

elaboration: tactic execution took 40.8s

[Yaël Dillies]

No waaay, does that work?

[Eric Wieser]

Yaël Dillies, fintype.card (finset (fin 6) × finset (fin 8)) is only 16384

[Stanislas Polu]

Fantastic!

[Eric Wieser]

That's well within the range of an exhaustive search

[Yaël Dillies]

To be fair, at the last olympic maths test we ran, some students tried 1000 cases one by one. 16k is much farther.

[Eric Wieser]

Possibly slightly more readable as

example :
  fintype.card {x : finset (fin 6) × finset (fin 8) //
                x.1.card ≡ x.2.card [MOD 4] ∧ 1 ≤ x.1.card + x.2.card} = 4095 :=

[Yaël Dillies]

Argh, I just updated my message to exactly this

[Kevin Buzzard]

Eric Wieser said:

That's well within the range of an exhaustive search

You say that, but I've seen Lean 3 fail to count to 10 before when it's also assembling proofs etc.

[Eric Rodriguez]

yeah, iirc dec_trival can barely handle the birthday problem

[Kevin Buzzard]

For $\binom{14}{0}+\binom{14}{2}+\binom{14}{4}+\binom{14}{6}$ the model answers seem to involve bashing it out, but using the Pascal's triangle identity you can rewrite as $\binom{13}{0}+\binom{13}{1}+\binom{13}{2}+\cdots+\binom{13}{6}$ which is half of $\sum_{i=0}^{13}\binom{13}{i}$ so is $2^{12}$.

[Kevin Buzzard]

So there could be some extension of this question where the numbers are much bigger then the generating function proof takes over.

[Stanislas Polu]

Now working on problem 16 which defines a list of numbers and asks for its median.

I was able to define this as a finset, but now am stuck to define the median? Maybe should I define this as a list and ask for the value of the element in the middle?

theorem amc12a_2021_p16
  (D : finset ℕ)
  (s : ℕ → finset ℕ)
  (m : ℕ → ℕ → ℕ)
  (h₀ : ∀ k x, m k x = k)
  (h₁ : ∀ n, s n = finset.image (m n) (finset.range n))
  (h₂ : D = finset.bUnion (finset.range 200) s) :
  0 = 0 :=
begin
  sorry
end

[Stanislas Polu]

uh, from reading more, finsets are sets in the sense that they don't have repeats, so that probably does not work

[Yaël Dillies]

You can use multiset instead, but yeah lists are a good idea too.

[Yaël Dillies]

Also, you can get rid of s like that:

theorem amc12a_2021_p16
  (D : finset ℕ)
  (m : ℕ → ℕ → ℕ)
  (h₀ : ∀ k x, m k x = k
  (h₂ : D = (finset.range 200).bUnion (\la n, (finset.range n).image (m n)) :
  0 = 0 :=
begin
  sorry
end

[Stanislas Polu]

Sorry, me again :grimacing:
Last question for the day! I can't seem to make this one work but I feel it's probably quite silly:

theorem amc12a_2021_p20
  (P : ℝ → set (ℝ × ℝ))
  (S : set ℝ)
  (h₀ : ∀ d, P d = { p : ℝ × ℝ | p.1^2 = 4*d*p.2 })
  (h₁ : S = { d : ℝ | ∃ a : (ℝ × ℝ), a ∈ (P d) → real.sqrt(a.1^2 + a.2^2) = 21 ∧ real.sqrt(a.1^2 + (d-a.2)^2) = 20 })
  (h₂ : fintype S) :
  S.to_finset.sum = 40/3 :=
begin
  sorry
end

This is refused by Lean with an error I have a hard time understanding. Also, Ideally I'd love to define (0, d) as a point and use a norm notation insted of real.sqrt(...) ?

This is the informal statement.

[Eric Wieser]

If I were you I'd replace P and S with standalone definitions, rather than take them as hypotheses

[Eric Rodriguez]

sum needs a function

[Eric Rodriguez]

I think you mean S.to_finset.sum id

[Eric Rodriguez]

open_locale big_operators will give you nicer notation :)

[Eric Rodriguez]

also, why do separate S : set ℝ and then a fintype on S instead of just S : finset ℝ?

[Yaël Dillies]

Join the finsect!

[Stanislas Polu]

Eric Rodriguez said:

open_locale big_operators will give you nicer notation :)

What do you have in mind ?

[Yaël Dillies]

Have a look for yourself! https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html

[Eric Rodriguez]

∑ x in S.to_finset, x

[Yaël Dillies]

And, once it will be a finset, ∑ x in S, x

[Stanislas Polu]

Eric Wieser said:

If I were you I'd replace P and S with standalone definitions, rather than take them as hypotheses

We've tried to keep statements self-contained so far but agreed it would be clearer.

[Stanislas Polu]

Eric Rodriguez said:

∑ x in S.to_finset, x

Ah makes sense :+1:

[Stanislas Polu]

Eric Rodriguez said:

also, why do separate S : set ℝ and then a fintype on S instead of just S : finset ℝ?

Hmmm I just tried that but the definition of S gets refused, (with or without the to_finset):

theorem amc12a_2021_p20
  (P : ℝ → set (ℝ × ℝ))
  (S : finset ℝ)
  (h₀ : ∀ d, P d = { p : ℝ × ℝ | p.1^2 = 4*d*p.2 })
  (h₁ : S = { d : ℝ | ∃ a : (ℝ × ℝ), a ∈ (P d) → real.sqrt(a.1^2 + a.2^2) = 21 ∧ real.sqrt(a.1^2 + (d-a.2)^2) = 20 }.to_finset) :
  (∑ x in S, x) = (40:ℝ)/3 :=
begin
  sorry
end

[Eric Wieser]

Here's how I might state it:

import data.real.sqrt
import algebra.big_operators.finprod

open_locale big_operators

theorem amc12a_2021_p20 :
  let P : ℝ → set (ℝ × ℝ) := λ d : ℝ, {p : ℝ × ℝ | p.1^2 = 4*d*p.2},
      S : set ℝ := { d : ℝ |
        ∃ a : (ℝ × ℝ), a ∈ P d → real.sqrt(a.1^2 + a.2^2) = 21 ∧ real.sqrt(a.1^2 + (d-a.2)^2) = 20 }
      in
  ∑ᶠ x ∈ S, x = 40/3 :=
begin
  sorry
end

[Yakov Pechersky]

That set notation only works on sets. You'd have to use finset.filter instead.

[Yaël Dillies]

How would it figure out that { d : ℝ | ∃ a : (ℝ × ℝ), a ∈ P d → real.sqrt(a.1^2 + a.2^2) = 21 ∧ real.sqrt(a.1^2 + (d-a.2)^2) = 20 } is finite?

[Eric Wieser]

You can't use filter because there's nothing finite to filter

[Yakov Pechersky]

If you really want to use norm, then there is L2 space over the reals.

[Eric Wieser]

What's that space called (in mathlib identifiers)?

[Stanislas Polu]

Eric Wieser said:

Here's how I might state it:

import data.real.sqrt
import algebra.big_operators.finprod

open_locale big_operators

theorem amc12a_2021_p20 :
  let P : ℝ → set (ℝ × ℝ) := λ d : ℝ, {p : ℝ × ℝ | p.1^2 = 4*d*p.2},
      S : set ℝ := { d : ℝ |
        ∃ a : (ℝ × ℝ), a ∈ P d → real.sqrt(a.1^2 + a.2^2) = 21 ∧ real.sqrt(a.1^2 + (d-a.2)^2) = 20 }
      in
  ∑ᶠ x ∈ S, x = 40/3 :=
begin
  sorry
end

Very nice

[Eric Wieser]

That still doesn't resemble the statement very well IMO

[Yaël Dillies]

You can also ad hoc give the two values, and have the statement be "This condition implies it's one of them" and "The sum of the two is 40/3"

[Yaël Dillies]

That's the problem with those statements. They ask you to calculate stuff, but the exercise isn't about calculating stuff.

[Eric Wieser]

docs#euclidean_space is the L2 space

[Stanislas Polu]

Eric Wieser said:

That still doesn't resemble the statement very well IMO

Welll agreed it's not perfect, but it's a good start! :)

[Yaël Dillies]

I think it's fair to formalise the mathy part of the exercises and leave the calculatory part (here, adding two numbers :rofl:) behind.

[Yaël Dillies]

Note that the original statement doesn't compile in my head either: "What is the sum of this potentially infinite number of solutions?"

[Stanislas Polu]

I guess it's a hint to restate as a quadratic equation and use Vieta's formula

[Yaël Dillies]

Of course. That's why you should allow yourself some freedom in formalising.

[Eric Wieser]

Is the question even well posed? Presumably it's asking for the sum of all unique lengths F V, but I could also sum the lengths over all possible F and V (which would be infinite due to translation / rotation)

[Eric Wieser]

This to me looks like the most faithful version of the statement:

def parabola (V F : euclidean_space ℝ (fin 2)) : set (euclidean_space ℝ (fin 2)) :=
sorry

theorem amc12a_2021_p20 (A : euclidean_space ℝ (fin 2)) :
  ∑ᶠ (d : ℝ) (h : ∃ V F : euclidean_space ℝ (fin 2), dist A F = 20 ∧ dist A V = 21 ∧ dist F V = d),
    d = 40/3 :=
begin
  sorry
end

[Eric Wieser]

Obvously it's much harder to prove because it's hasn't performed any of the steps like "well obviously we can put V at the origin and F on the positive y axis"

[Stanislas Polu]

Indeed, though your statement is ambiguous as it relies on the "informal" knowledge of what a parabola is and cannot be automatically checked without a human checking that the definition for parabola matches an actual parabola?

[Eric Wieser]

It stops being ambiguous once you fill out the sorry, doesn't it?

[Eric Wieser]

Did you check the definition of ℝ matches the actual reals, or were you happy to trust mathlib ;)

[Stanislas Polu]

oh! you meant filling the parabola definition first and then providing the theorem as goal :+1: