## Stream: new members

### Topic: Finding out the Natural Language of a theorem in Mathlib

#### Jack Heseltine (Jul 10 2023 at 02:40):

I am specifically wondering what this theorem means, but new to Mathlib and not googling successfully at the moment. Can someone point me to the correct way to find out about a question like this?

theorem prime . dvd_of_dvd _pow {p m n : ℕ} (pp : prime p) (h : p \[Divides] m^n) : p \[Divides] m :=
begin
induction n with n IH,
{ exact pp . not_dvd_one . elim h },
{ rw pow_succ at h, exact (pp . dvd_mul.1 h) . elim id IH }
end

#### Kevin Buzzard (Jul 10 2023 at 04:02):

It means that if $p$ is prime and $p|m^n$ then $p|m.$

#### Scott Morrison (Jul 10 2023 at 07:03):

@Jack Heseltine, there's not a general method for getting help with "what is the natural language version of this statement", beyond learning the basic Lean syntax so you can do it yourself, or asking here.

#### Scott Morrison (Jul 10 2023 at 07:04):

#3808 is a PR proposing a helper function for the opposite direction (i.e. a #formalize command), but it will only be useful for people either with GPT API access, or a locally running LLM. We could very easily add the other direction, as well.

#### Johan Commelin (Jul 10 2023 at 07:04):

Where does the \[Divides] syntax come from?

#### Scott Morrison (Jul 10 2023 at 07:04):

I think this text has been copied and pasted via Mathematica.

#### Scott Morrison (Jul 10 2023 at 07:05):

It rewrites Unicode in interesting ways (and is also prone to insert spaces around punctuation!)

#### Kevin Buzzard (Jul 10 2023 at 09:47):

import Mathlib.Tactic

namespace Nat

theorem prime.dvd_of_dvd_pow {p m n : ℕ} (pp : Prime p) (h : p ∣ m^n) : p ∣ m := by
induction' n with n IH
{ exact pp.not_dvd_one.elim h }
{ rw [pow_succ] at h; exact (pp.dvd_mul.1 h).elim IH id }
done


is something which you can just cut and paste into Lean 4.

#### Alex Kontorovich (Jul 10 2023 at 14:29):

If you have ChatGPT, you can get a much quicker answer by asking it directly (no guarantee that what it's saying is right, but it might give some useful hints). E.g.:
image.png

Last updated: Dec 20 2023 at 11:08 UTC