By schoolkid

Stream: maths

[Chris Hughes]

A 12 year old just got a prize for proving this.

example : ∀ n : ℕ, 7 ∣ n ↔ 7 ∣ (n / 10 + 5 * (n % 10))

This can be turned into a Presburger formula right? Should omega be able to do it?

I tried turning it into a Presburger formula, but it didn't seem to work.

import tactic.omega
open nat
example (n : ℕ) : 7 ∣ n ↔ 7 ∣ (n / 10 + 5 * (n % 10)) :=
begin
  rw [dvd_iff_mod_eq_zero, dvd_iff_mod_eq_zero],
  have := nat.mod_lt n (show 0 < 7, by norm_num),
  have := nat.mod_add_div n 7,
  have := nat.mod_lt n (show 0 < 10, by norm_num),
  have := nat.mod_add_div n 10,
  have := nat.mod_lt (n / 10 + 5 * (n % 10)) (show 7 > 0, by norm_num),
  have := nat.mod_add_div (n / 10 + 5 * (n % 10)) 7,
  repeat { revert this },
  generalize : n % 7 = a,
  generalize : n / 7 = b,
  generalize : n / 10 = c,
  generalize : n % 10 = d,
  generalize : (c + 5 * d) % 7 = e,
  generalize : (c + 5 * d) / 7 = f,
  omega -- doesn't work
end

12-year-old Nigerian boy based in the UK, Chika Ofili, has been presented with a Special Recognition Award for making a new discovery in Mathematics. The little Mathematician just discovered a new formula for divisibility by 7 in Maths. https://twitter.com/SplufikNG/status/1193786365059534849/photo/1

- NG to the World (@SplufikNG)

[Kevin Buzzard]

I would not be surprised if you could find some previous reference to this test in some popular maths book from the 50s, it's very dangerous calling it a new formula. But good on him. It's 7|10x+y iff 7|x+5y. If you apply the test to 14 you get 21.

[Abhimanyu Pallavi Sudhir]

It's m | a x + b y iff m | (an-br) x + bn y for hcf(m, n) = 1 (or something like that). I think this stuff is taught in high school.

[Abhimanyu Pallavi Sudhir]

What's omega?

[Johan Commelin]

A tactic that proves statements in the language of the ordered group of integers

[Johan Commelin]

So you are allowed to add and compare integers using ≤ but you can only multiply with constants