Offering hourly contract work converting proofs to Lean

Stream: job postings

[Alex Altair]

Hi all! Basically what it says on the tin; I often work with a theorem in a paper and wish to myself that I could have a Lean-ified version of it to sanity-check my understanding, and to test out variations. I'd love to have someone who I can pay to produce such proofs! These theorems are often relatively small and simple, and so I don't think it would necessarily take tons of hours to e.g. encode all the background math into mathlib.

You can message me about it here, although I'm more likely to see your message if you email me at alexanderaltair@gmail.com