Is lean the right tool for me

Stream: new members

[Oleg Sunok]

Thank you for your excellent tutorial (The Natural Number Game). I'm a programmer, not a mathematician, and in the search for the right hypothesis checking system, I was only able to gain a foothold here, because all the others were written by mathematicians for mathematicians. However, before I delve into the subject further, I would like to know whether it is really the right tool for me. My work is not about testing mathematical theorems, but rather determining various hyphoteses about certain series of numbers, for example on {1,5,2,8,7 ..}, whether and how often n(x) is even if n(x-1)-n(x-2) > 3. Is it possible with Lean? If not, can you recommend the right tool for me?

[Huỳnh Trần Khanh]

were written by mathematicians for mathematicians

wrong, other theorem provers are not written by proper mathematicians for proper mathematicians. they are written by descendants of Zermelo, Fraenkel, Dedekind, Russell, Gödel and the like. from what I've gathered, most mathematicians don't really care about foundations. interactive theorem provers are written by experts that are really familiar with arcane foundational stuff. and you have to adopt a different mental model to use interactive theorem provers effectively.

various hypotheses about certain series of numbers

well... I don't get what you mean. this is pretty vague, can you explain?

[Johan Commelin]

Oleg Sunok said:

I was only able to gain a foothold here, because all the others were written by mathematicians for mathematicians.

Lol, usually the complaint is that all the tutorials are written by computer scientists for computer scientists...

[Oleg Sunok]

Huỳnh Trần Khanh said:

various hypotheses about certain series of numbers

well... I don't get what you mean. this is pretty vague, can you explain?

I thought my example would be the explanation, but I might try this: the tutorial is based on the set of natural numbers, sorted - and I have to do with rows of numbers that represent certain observations (time series) and have to be validated on various hypotheses from specialist departments

[Johan Commelin]

Lean can certainly handle that. But so can any other proof assistant.

[Johan Commelin]

If this is tied to some algorithm, if you want to do software verification, then you might want to consider Coq as well.

[Johan Commelin]

They have a lot of infrastructure for this kind of stuff.

[Johan Commelin]

In what language are you writing your code?

[Oleg Sunok]

Johan Commelin said:

In what language are you writing your code?

C# or Javascript. I can program it "native", but I want to find something that can check my program logic quickly. Coq has put me off.

[Johan Commelin]

Ok, so there will be a human component: translating between C#/JS and something like Lean.

[Johan Commelin]

This can of course be a source of error. As long as you are aware of it, I won't complain.

[Johan Commelin]

Learning Lean requires a bit of effort. But it is certainly up to the task that you sketched.

[Johan Commelin]

Btw, #tpil might be more what you are looking for. I think it's written with more of a CS audience in mind.

[Anne Baanen]

I would also recommend the Hitchhiker's Guide to Logical Verification :)

[Johan Commelin]

Can a zulip admin create #hglv for us?

[Mario Carneiro]

Oleg Sunok said:

My work is not about testing mathematical theorems, but rather determining various hyphoteses about certain series of numbers, for example on {1,5,2,8,7 ..}, whether and how often n(x) is even if n(x-1)-n(x-2) > 3. Is it possible with Lean? If not, can you recommend the right tool for me?

It sounds like what you want is not a proof assistant at all, but rather a computer algebra system like Sage or Mathematica. Unless you are interested in proving your conjectures once you have them, the proof assistant isn't that much of a value add. CAS's are much better for experimental mathematics.

[Scott Morrison]

#hglv