Discussion "lean gig available"

Stream: general

[Joachim Breitner]

I assume if you were willing to share your proof, you'd have done it right away, right? Can you at least indicate how long the informal proof is? And maybe let us know if your proof is resolving some long standing open conjecture or question, or if it is something more niche?

[Paul Stahura]

i dont know how to answer your question. I don't know what "right away" means. I am an recreational math person. I came up with a conjecture. i checked it numerically using a million randomly generated points and A(s) and B(s) matched up to 10 places after the decimal. that gave me confidence to attempt a proof. that took me about a month. its not a long standing, or even short standing, open conjecture. one of the functions, lets call it A(s), is well known. i've typed the proof into overleaf.com and the resulting pdf for the proof part is 6 pages.

[Paul Stahura]

I'm new to Lean, too. I only learned about what Lean can do (was already familiar with the proof assistant concept beforehand) last week after attending the JMM conference which happened to take place in Seattle near where I live.

[Joachim Breitner]

6 pages of informal proof can be rather intense to formalize, depending on the level of detail and the amount of theory it uses that may still be missing from mathlib – but if you find someone who is interested and they can look at it they will tell you more.

Also, your deal should also say what happens (compensation wise) when during the formal verification it turns out that the the proof was not correct.

[Jireh Loreaux]

Paul, since the function A(s) is well-known, do you mind sharing what that is? This could give someone a (small) hint about how much work it would be to do what you're asking. (e.g., if it's a well-known function for which we have some API in Mathlib, that's more doable. If we haven't even formalized the definiton of A(s) yet, then you're really asking for two separate things to some extent.)

[Paul Stahura]

i didnt realize these messages were public I thought they were DMs so i deleted the last 2

[Paul Stahura]

Joachim Breitner to answer your question, I will pay for the person's time up to the point that they find out the formal verification turned out that my proof was not correct (and explain to me why that is the case). Also, as i said in my first post I'll pay 1/2 the estimate up front.

[Andrés Goens]

Discussion thread for #job postings > Lean gig available

[Andrés Goens]

Maybe this should be moved to a "discussion" thread? (I've always interpreted this #job postings stream to be similar to announce). I wanted to do it myself (#general > Discussion "lean gig available" ) but it turns out I don't have permisions to move messages (somehow I thought everyone had)

[Notification Bot]

8 messages were moved here from #job postings > Lean gig available by Johan Commelin.