AI-assisted formalization of OEIS A053819, feedback welcome

Stream: new members

[Touko]

Hey, I used Claude to formalize OEIS A053819 (sum of cubes of totatives divisible by n). It compiles, proof uses the standard pairing argument.

https://github.com/ToukoUrsin/oeis-a053819-lean

Is AI-generated stuff welcome in the Archive? Happy to hear if this is weird or not.

[Michael Rothgang]

Hi and welcome! The mathlib archive is meant for proofs showcasing Lean's and mathlib's features --- in particular, there is a high bar on idiomatic and readable code. At the moment, typical AI code is very far from this; I expect yours to be the same (but haven't checked).

[Michael Rothgang]

The path towards getting your code into mathlib-ready shape starts with lots of learning about idiomatic code. Learning without AI, I dare say --- because "just AI" is simply not good enough right now. Take some code, try to formalise it, get feedback, read other idiomatic code, learn from experienced contributors here... expect this process to take months. Then, you can hope to be able to know more Lean and write closer to idiomatic code. This journey is very possible (I myself learned a lot from having my code reviewed by experienced contributors), but requires you to learn and write Lean code by hand.

[Michael Rothgang]

(The final question is whether this OEIS relation is in scope for the mathlib archive. I'm not sure, to be honest. It doesn't appear to contribute or be linked to interesting theory.)

[Kevin Buzzard]

The proof is that for $n>2$ we have $\sum_{gcd(i,n)=1}i^3=\sum_{gcd(i,n)=1,i<n/2}(i^3+(n-i)^3)$ which is obviously a multiple of $n$ because each summand is $i^3+(-i)^3$ mod $n$ which is 0; the proof generalises to any odd power, it's not some weird fact about 3, and mathlib would probably only accept a proof in the right level of generality.

Your code is maybe 2-3 times as long as it should be, e.g.

theorem dvd_cube_pair (n k : ℕ) (hk : k ≤ n) : n ∣ k ^ 3 + (n - k) ^ 3 := by
  zify
  rw [cast_sub hk]
  use n^2-3*n*k+3*k^2
  ring

is a far cleaner way to prove dvd_cube_pair and a lot of the other code goes a bit around the houses too.

In general, as Michael said, it's currently extremely difficult to get AI-generated code into mathlib unless it's tidied up by an expert afterwards.

[Snir Broshi]

How about https://provables.github.io/sequencelib/ ?

[Walter Moreira]

Please, check out the contributing guidelines for Sequencelib at https://provables.org/sequencelib/getting_started/contributing/ . We would be happy to work with you to add your formalization. It probably will require some clean-up and adjusting to our project scaffolding, but shouldn't be too much work. We started Sequencelib precisely as a way to collect this type of formalizations of the OEIS that don't contribute to a big theory at the moment.