Big Integers intro questions

Stream: new members

[Ian Allen]

I work on the Collatz and I am here for a number of reasons: 1) Lean as a data analysis assistant -with GMP BigInt capabilities- to replace my current software, 2) Lean as a repository for my collected work, and 3) Lean as a proof assistant not only for the first clause, but for eventual publication if I get that far.

So first thing I did was start searching threads but I cant get any hits on my keywords. Therefore I ask if anybody has anything to point me in the right direction especially with the first two points, which focus on how to actually do investigative work with lean (with big integers!), and how to keep that information recorded in a tidy fashion. I will read anything.

An example of the kind of software assisted work I do currently, is to use iterative algorithms to compute collatz transforms on any class of numbers of interest, and then display the data either in spreadsheet (common) or graphs (less common but still important), and sieve thru it all looking for points of interest. Then reprogram as needed, rinse, and repeat.

Yes, I am aware this problem is impossible. I don't care. It is fun, it is beautiful, and it keeps me busy. :D