# Zulip Chat Archive

## Stream: maths

### Topic: By schoolkid

#### Chris Hughes (Nov 13 2019 at 00:57):

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 (Nov 13 2019 at 07:33):

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 (Nov 14 2019 at 19:34):

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 (Nov 14 2019 at 19:34):

What's `omega`

?

#### Johan Commelin (Nov 14 2019 at 19:34):

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

#### Johan Commelin (Nov 14 2019 at 19:35):

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

Last updated: May 14 2021 at 20:13 UTC