Lean tutoring job

Stream: general

[Alex Meiburg]

Job opportunity: teaching Lean for $50/hr

So in an online forum, someone was trying to share their proof of the Collatz conjecture, and other people weren't really interested in reading it. I suggested that, since the proof looked fairly short and elementary, they could try formalizing it in a proof assistant like Lean, and if it passed, then surely this would get the attention and credibility of mathematicians; and that even if the proof didn't work out, that learning Lean could help with improving their own mathematical thinking -- with the admission that this was a somewhat tall order since they have to learn a whole programming language. Somewhat to my surprise, they responded positively, and said they would like to pay someone $50/hr to tutor them in Lean.

Personally I'm too busy, but if this sounds like a job you would like let me know and I'll put you in touch. As a disclaimer, I don't really know anything else about this person besides their name.

[Kim Morrison]

Being paid to check "proofs" of FLT or Goldbach was a time honoured tradition at the Berkeley PhD program. For it to be tolerable you needed to make sure that the person paying was sane enough that they would accept "here is the first error or meaningless statement" and then go away and do their thing. Great example of technology making jobs obsolete, as Lean does this for free now. :-)

[Alex Meiburg]

Yes, I don't know what the level of patience would be, it might not go well. But it could be interesting to a grad student needing some money, so I decided to put it here. :)

[Chris Birkbeck]

I got tired of these emails, so I made a lean 3 "game" (https://cbirkbeck.github.io/lean-game/?world=2&level=1) which I could send them and say "great, could you type up your proof in lean here". Never heard back from anyone though.