Zulip Chat Archive

Kevin, I do not know if Johan's comment was an answer to your question, but for me, the success rate for library_search increased a lot once I had an expectation of what lemmas it might find. For instance, I now know that with inequalities, if I have < in context and the result follow for \le, then library_search will likely work with have : \le := le_of_lt, but probably not otherwise.

A few months back, I would have simply said: "oh well, library_search is not helping me".

However, I am still intimidated by how to use gptf and, even though I would like to use it, I am afraid of installing it and breaking what I think is a fragile equilibrium of git and lean working at the same time! :upside_down:

Johan Commelin (Jun 28 2021 at 07:22):

My "yes" was a reply to Alex

Julian Berman (Jun 28 2021 at 07:36):

gptf can produce non-syntactically valid output (or syntactically valid but nonexistant lemma output), so I suspect it may confuse more than help for very new folks even though it is certainly super cool

Julian Berman (Jun 28 2021 at 07:37):

I can say though Damiano that I managed not to break anything by just putting it in a separate repository, it wants lean 3.26 anyhow IIRC, so that part at least I think is surmountable, it's definitely cool to play with

Alex Zhang (Jun 28 2021 at 08:15):

Does anyone know how long I usually need to wait to get an API key before starting trying this?

Kevin Buzzard (Jun 28 2021 at 08:18):

I think mine took about a week to arrive, I wouldn't hold your breath :-)

Huỳnh Trần Khanh (Jun 28 2021 at 08:20):

Alex Zhang said:

Does anyone know how long I usually need to wait to get an API key before starting trying this?

a week and the email looks like this, initially i didn't even know that i received an api key lol because the email was... so vague
anyway if you see something like this it means you received an api key and you should follow the instructions Screenshot-from-2021-06-28-15.18.25.png

BANGJI HU (Nov 01 2024 at 02:21):

I want to formalize some problems, but first how to turn this proposition into code, especially how to deal with the maximum value

BANGJI HU (Nov 01 2024 at 02:22):

here is the problem
Let n be a positive integer. All numbers m which are coprime to n all satisfy m^6 = 1 (mod n) . Find the maximum possible value of n.

Notification Bot (Nov 01 2024 at 02:35):

2 messages were moved here from #mathlib4 > mod by Kim Morrison.

BANGJI HU (Nov 01 2024 at 02:58):

finally

import Mathlib.Data.Nat.Count
import Mathlib.Data.Nat.Defs
import Mathlib.Data.Nat.Digits
import Mathlib.Data.Nat.Dist

import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Data.Nat.GCD.BigOperators

import Mathlib.Data.Nat.MaxPowDiv
import Mathlib.Data.Nat.ModEq

import Mathlib.Data.Nat.Prime

import Mathlib.NumberTheory.Modular
def Nat.coprime (m n : Nat) : Prop := Nat.gcd m n = 1

theorem max_coprime.sixth_power_mod :
  ∃ n : ℕ, (∀ m : ℕ, Nat.coprime m n → m^6 ≡ 1 [MOD n]) ∧
  (∀ k : ℕ, k > n → ∃ m : ℕ, Nat.coprime m k ∧ ¬(m^6 ≡ 1 [MOD k])) := by
  -- 证明504满足条件
  use 504
  constructor

BANGJI HU (Nov 01 2024 at 08:08):

import Mathlib.Data.Nat.Count
import Mathlib.Data.Nat.Defs
import Mathlib.Data.Nat.Digits
import Mathlib.Data.Nat.Dist
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Data.Nat.GCD.BigOperators
import Mathlib.Data.Nat.MaxPowDiv
import Mathlib.Data.Nat.ModEq
import Mathlib.NumberTheory.Modular


def Nat.coprime (m n : Nat) : Prop := Nat.gcd m n = 1

theorem max_coprime_sixth_power_mod :
  ∃ n : ℕ, (∀ m : ℕ, Nat.coprime m n → m^6 ≡ 1 [MOD n]) ∧
  (∀ k : ℕ, k > n → ∃ m : ℕ, Nat.coprime m k ∧ ¬(m^6 ≡ 1 [MOD k])) := by
  -- n = 2^3 * 3^2 * 7
  use 504
  constructor

  · --504 satisfy
    intro m hm
    have h1 : m^6 ≡ 1 [MOD 8] := sorry
    have h2 : m^6 ≡ 1 [MOD 9] := sorry
    have h3 : m^6 ≡ 1 [MOD 7] := sorry
    sorry

  · --for n >504
    intro k hk

    use 2
    constructor
    ·
      sorry
    ·
      sorry

Eric Wieser (Nov 01 2024 at 12:16):

Are you looking for docs#IsGreatest ?

edklencl (Nov 01 2024 at 13:40):

i.suppose it has.something todo with fermat little theory

Last updated: May 02 2025 at 03:31 UTC