3k+1 experiment - plugin for maps / feature

Stream: new members

[Michael Bucko]

I wrote (with a big red sorry) this:

import Mathlib

partial def collatz : ℕ → ℕ
| 1 => 1
| n =>
  if n % 2 == 0 then
    collatz (n / 2)
  else
    collatz (3 * n + 1)

def collatz_iter : ℕ → ℕ → ℕ
| 0, n     => n
| (k + 1), n => collatz_iter k (collatz n)

theorem collatz_iter_one (k : ℕ) : collatz_iter k 1 = 1 :=
  sorry

I want to explore it in a semi-automated way based on my insights. I have a couple of ideas related to:

• dynamical systems concepts and defining some sort of dynamical maps
• random walk models and density concepts
• graph construction and invariants

Now, I'd like to get like a map based on what's available in mathlib4 of the options, even if that's all filled with sorry's. That'd be very helpful.

Does there exist a plugin based on mathlib4 and Lean4 data (with settings where I could add my LLM keys) that I could use?

LLMs are not good enough at this yet. Still, that's a weaker use case where the human insight needs to be stronger (and the LLM can be "fuzzier"), and the quality of the map does not need to be perfect (because one can't yet expect that the LLM will generate the working code (it might change))

[Edward van de Meent]

i think you might be misunderstanding what your collatz does; due to the recursion, it already does steps untill it gets to 1

[Edward van de Meent]

to the point that the collatz conjecture is equivalent to proving that this function collatz terminates.

[Edward van de Meent]

due to this, your collatz_iter is likely of no use to you

[Michael Bucko]

Yes, I am just learning Lean, so feel free to help me correct the code too. Any help would be appreciated!

[Edward van de Meent]

likely, you instead want the following definition for collatz:

def collatz : ℕ → ℕ
| 0 => 1
| 1 => 1
| n =>
  if n % 2 == 0 then
    (n / 2)
  else
    (3 * n + 1)

[Edward van de Meent]

this does a collatz-step when n is not 0 or 1, otherwise gives 1

[Edward van de Meent]

the collatz conjecture would then be that for any n there is a y such that collatz_iter y n = 1

[Edward van de Meent]

i forgot 0 is a natural number, oops :upside_down:

[Michael Bucko]

Btw. I think the reason for that iterator was that I somehow couldn't apply that function multiple times within the theorem statement..

@Edward van de Meent Is the reason you're not doing this as a recurrent function that it's somehow not possible to define a theorem like this?

[Edward van de Meent]

from my understanding, by saying partial you lose a lot of theorem proving power about what value this function takes

[Michael Bucko]

(my understanding is very limited) I use partial because of something like this: "I am not sure it'll terminate, and I want it to make the code work asap". I guess I could remove that thing knowing that 3k+1 sequence eventually gets to 1?

[Michael Bucko]

I'm not sure I can even remove partial from this theorem -- if that's the case, perhaps you really need to iterate and can't use a recurrent function? But I don't know.

[Edward van de Meent]

for the sake of clarity: the following is how one might formalize the statement of the collatz conjecture. (no proof)

import Mathlib
/-- do a single collatz-step. `collatz_step n` returns 1 if `n < 2`, otherwise `n/2` if `n` is even, otherwise `3 * n + 1`-/
def collatz_step (n : ℕ) : ℕ :=
  if n % 2 == 0 then
    (n / 2)
  else
    (3 * n + 1)

/-- `collatz_iter k n` does `k` collatz-steps on `n` -/
def collatz_iter : ℕ → ℕ → ℕ
| 0, n     => n
| (k + 1), n => collatz_iter k (collatz_step n)

#eval collatz_iter 986 670617279 -- this number gets to 1 only after 986 steps

theorem collatz_conjecture : ∀ (n : ℕ), n = 0 ∨ ∃ k, collatz_iter k n = 1 :=
  sorry

note that there is no need for partial here.

i do not understand what theorem using partial you mean?

[Michael Bucko]

Yes, so your line is step - iterate - use the iter in the theorem definition. Is there a way to use a recurrent function in the definition, i.e. can one also use the existing recurrent function in the theorem?

As for partial, I was getting errors related to the function potentially not terminating, so I learnt to use partial and noncomputable.

[Yakov Pechersky]

collatz_iter is basically "collatz with a fuel parameter". So it is recurrent up to fuel steps.

[Edward van de Meent]

i don't really think it makes sense to make a function that iterates these steps...

[Edward van de Meent]

there is no clear criterion for when to stop, or there is no proof that that criterion will always be met after some number of iterations.

[Yakov Pechersky]

If you don't want to define a separate step function, you can inline it:

def fueled_collatz : ℕ → ℕ → ℕ := fun
  | 0, n => n
  | (fuel + 1), n => fueled_collatz fuel (go n)
  where go : ℕ → ℕ := fun n ↦
    if n % 2 == 0 then
      (n / 2)
    else
      (3 * n + 1)

[Michael Bucko]

Edward van de Meent schrieb:

i don't really think it makes sense to make a function that iterates these steps...

You are actually using collatz_iter in your snippet.

[Michael Bucko]

Yakov Pechersky schrieb:

If you don't want to define a separate step function, you can inline it:

def fueled_collatz : ℕ → ℕ → ℕ := fun
  | 0, n => n
  | (fuel + 1), n => fueled_collatz fuel (go n)
  where go : ℕ → ℕ := fun n ↦
    if n % 2 == 0 then
      (n / 2)
    else
      (3 * n + 1)

I'll try it out. Didn't know how to inline it.

[Edward van de Meent]

Michael Bucko said:

Edward van de Meent schrieb:

i don't really think it makes sense to make a function that iterates these steps...

You are actually using collatz_iter in your snippet.

yes, but i got the sense that that definition was not what you're interested in?

[Edward van de Meent]

since you wanted recurrence in the definition?

[Michael Bucko]

Edward van de Meent schrieb:

Michael Bucko said:

Edward van de Meent schrieb:

i don't really think it makes sense to make a function that iterates these steps...

You are actually using collatz_iter in your snippet.

yes, but i got the sense that that definition was not what you're interested in?

No, I think it's completely fine to do it like this :thank_you:

I was just wondering whether there's a more concise way, without iterating these steps as a separate function.

Looking into that inlining now.

[Michael Bucko]

@Yakov Pechersky #eval fueled_collatz 986 670617279 gives me 1. So not only don't I need partial, but can also re-use my recurrent implementation.

Didn't know how to do it! Thank you

[Michael Bucko]

So the definition is great now.

How about the next step? Let's say I want to create a dynamical system-based model of the chains starting at the 3k+1 seed.

And I don't want to ask LLMs directly -- because I don't think they'll be that helpful at the moment (this will change).

Does there exist any mathlib4 assistant plugin (I am already using Loogle, Moogle, Duper, LeanDojo, and so on) that could recommend certain basic (or more advanced) concepts / proof lines from other mathlib4 proofs?

[Kyle Miller]

partial causes the definition to become completely opaque, meaning it would be impossible to unfold it. It's a keyword mainly useful for programming purposes.

Like Edward said, being able to convince Lean that partial is not needed for the first version of collatz is the same thing as proving the Collatz conjecture :-)

[Edward van de Meent]

(assuming you add the 0-clause. if you don't, you're proving lean inconsistent!)

[Michael Bucko]

Kyle Miller schrieb:

partial causes the definition to become completely opaque, meaning it would be impossible to unfold it. It's a keyword mainly useful for programming purposes.

Like Edward said, being able to convince Lean that partial is not needed for the first version of collatz is the same thing as proving the Collatz conjecture :-)

Perfect. I eventually didn't have to use it.

[Michael Bucko]

@Edward van de Meent The 0-clause should be there. Btw. check out this from @Yakov Pechersky - that's already included.

def fueled_collatz : ℕ → ℕ → ℕ := fun
  | 0, n => n
  | (fuel + 1), n => fueled_collatz fuel (go n)
  where go : ℕ → ℕ := fun n ↦
    if n % 2 == 0 then
      (n / 2)
    else
      (3 * n + 1)

[Michael Bucko]

So, let's say I want to create a dynamical system-based model of the chains starting with the 3k+1 seed.

Does there exist any mathlib4 assistant plugin that could recommend certain basic (or more advanced) concepts / proof lines from other mathlib4 proofs?

LLMs currently give me concepts like, which is a bit inspiring, but also feels way too superficial atm (they will get better) (some examples below) I'd need something that understands mathlib4 very well.

def orbit (n : ℕ) : ℕ → ℕ | 0 => n | (k+1) => collatz (orbit k)

theorem only_trivial_cycle : ∀ n k : ℕ, is_cycle n k → n = 1 := by

theorem collatz_stable_fixed_point : is_stable_fixed_point 1 := by