Zulip Chat Archive

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 :=
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 }

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

It means that if pp is prime and pmnp|m^n then pm.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 }

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.:

Last updated: Dec 20 2023 at 11:08 UTC