Suitable problem for Lean? & Paid Consulting help?

Stream: new members

[North Eastern Ohio Mac Developer]

Hi,

My background consists of a computer science degree and 10+ years work as a software engineer (although I've been mostly out of work the last 8 years for health issues), admittedly my mathematical background is very weak, and all my work experience is basically doing Mac GUI app development nearly all in Objective-C. Around 7 years ago I made an observation in the number theory domain that I keep coming back to and trying to figure out how to prove, but have been unable to do so yet. When I heard of AlphaProof & Lean it seemed worth looking into as an approach to find a proof.

However, in all honesty, after 3 hours of skimming the Lean website and documentation I haven't been able to figure out the first thing about how to get to a point of being able to run anything. I downloaded the binaries from GitHub, but couldn't find anything that would guide me through how to integrate into an Xcode project, or even just a HelloWorld type project able to be done direct from a command line without IDE integration.

In light of my difficulties getting started with Lean, I guess I really just want to try and get two questions answered here. First, I'd like to describe the number theory observation I have in mind and hear some opinions on whether this is a suitable problem to try to use Lean for generating a proof. Secondarily, I'd like to ask if there are any parties out there interested in taking on a small project of helping me investigate this question using Lean. (Open to providing a reasonable small amount of compensation.)

I don't want to provide the exact details here, so I'm intentionally being a bit vague or obtuse, but here is essentially the situation:

There is a type of well documented number in the math literature where it's divisors have a particular form. So like N1 has divisors q1, q2, q3, and N2 has divisors q4, and q5, where the q divisors all have a precise form that I'll leave out of this discussion. Furthermore it's a basic algebraic observation that N1 and N2 can be combined to form a new number like N3=N1xN2xC. In years of researching the math literature, nothing I ever read ever says anything about the properties of C. But about 7 years ago I noticed that the divisors of C also have a nearly the same precise form that the q divisors for N have. And if I look at the proofs available for why N has divisors with the form of the q numbers I can't ever figure out how to extrapolate it to show that C has divisors with essentially the same form. Over the years I've written programs to factor lots of these large N numbers and build tables of the results, and I can never find a counter-example where C doesn't have a divisor with the form like q. But I don't know how to PROVE the divisors of C have to only have divisors with the same form as the q divisors like the N numbers.

That description was probably very hard to follow, since I'm intentionally trying to leave of precise details. Sorry. So my question to those in the know about Lean are:
1) Is this a suitable problem for investigation with Lean? Or is there some reason why this would be unlikely to yield a meaningful result?
2) Is there anyone out there interested in discussing this further with me, and potentially writing up some Lean code to investigate? Or alternatively, consider it some consulting work to help guide me through getting started with Lean and reach the point I can investigate this on my open. I'm open to providing some reasonable small compensation for your time. Basically, I just suspect trying to come up to speed on my own with Lean is going to be a but of a Herculean effort when it's so different from the type of development I've done in my background.

Feel free to reply here, or get it touch via the e-mail in my user profile. Thank you.

[Muizzi]

Hey, Lean is used to verify and check proofs. Lean does not generate proofs.

[North Eastern Ohio Mac Developer]

Ahhh! Well, that's vastly different than the impression I came away with from reading the article about AlphaProof. Thank you.

[Mario Carneiro]

@North Eastern Ohio Mac Developer AlphaProof is generating proofs, using Lean to ensure it doesn't generate nonsense. This work is very experimental and AFAIK does not exist in a form that is being distributed to users. In a sense it's not really what lean "was designed for", although that's no reason not to try it anyway (and if you visit #Machine Learning for Theorem Proving you can learn about a bunch of similar projects attempting to generate lean proofs, some of which you can use today). But for the most part, writing lean is like writing in any other programming language: you are the one who writes the code / proves the theorem, although the computer will help in a bunch of ways, and some tactics straddle the border between fully automated theorem proving and interactive theorem proving. But for an experimental question like the one you have here, I think you should use other methods to try to get closer to a proof sketch first, and then Lean will be useful for keeping track of the structure of the proof and ensuring you don't make subtle mistakes.