Looking for a Lean 4 instructor (paid)

Stream: job postings

[Simon Rubinstein-Salzedo]

I’m looking to hire one instructor to teach a course on mathematics in Lean for high-school students at Euler Circle.

Program info: https://eulercircle.com/

Some of the students will have very strong mathematical backgrounds at the level of advanced undergraduates, while for others this will be their first serious introduction to proof-based mathematics.

Requirements (non-negotiable):

• Solid experience with Lean 4
• Familiarity with mathlib
• Comfort formalizing real mathematics (not just toy examples)
• Ability and willingness to teach and explain proofs clearly
• Physically located in the United States and eligible to work without employer sponsorship (i.e. US citizen or permanent resident)

Ideal background:

• Graduate student, postdoc, or professor who actively uses Lean for serious mathematics

Role details:

• Teaching role
• Audience: highly motivated, advanced high-school students
• Expectation: you will be responsible for designing and teaching the class, and taking care of logistics to make sure that it runs smoothly
• Remote
• Course structure is flexible, but my current model is: 4 days/week for 5 weeks, ~2 hours per session
• Class times are flexible and can be scheduled to work well for the instructor

Compensation:

• $6000 total, with flexibility to increase if the workload turns out to be substantially higher than expected

If interested, please send me an email to me (Simon Rubinstein-Salzedo) at simon@eulercircle.com with:

• A brief description of your Lean experience
• Links to relevant GitHub / mathlib contributions (if any)
• A CV or short summary of prior teaching experience

I only need one person, so I’m prioritizing depth, clarity, and fit over speed.