Lean gig available

Stream: job postings

[Paul Stahura]

I'm looking for a consultant to use Lean to verify my proof.  This is a paid "work for hire" part-time side gig for a student, or anyone, who knows Lean.

I have two complex valued functions, call them A(s) and B(s), and i have a proof that A(s)=B(s) where I did not using Lean to make the proof, and I want someone to use Lean to show that A(s)=B(s) is true. I'm writing a paper which would include my proof, but it is extensive and I'd rather not have readers of the paper have to each go through my proof. I'd rather just provide the Lean proof to them.  I have the formulas for A(s) and B(s) in python, Latex, and Mathematica format.

I'd like to get on a zoom call with you, explain the details of the functions to you (and show you my proof), and for you to tell me approximately what it would cost (time and $) for you to show that A(s)=B(s) using Lean. I'll pay you 1/2 up front and 1/2 at the end.  If you are in the Seattle area, we can meet in person too, if you'd like.

[Notification Bot]

8 messages were moved from this topic to #general > Discussion "lean gig available" by Johan Commelin.