Lean 4 Mathematical Formalization Expert $170-200

Stream: general

[Alexander Pimentel Gomez]

Alignerr – Labelbox | Remote (Global)

Alignerr–Labelbox is hiring Lean 4 experts to support frontier AI training projects focused on mathematical reasoning, formal verification, and logic.

You are invited to consider applying if you are interested in working on one or more of the following areas, or closely related topics:

• Mathematical formalization in Lean 4
• Translating informal mathematics (textbooks, articles, exercises) into formally verified Lean 4 code
• Formal logic, verification, and automated reasoning
• Proof assistants and formal methods
• AI and machine learning for theorem proving and mathematical reasoning

---

What you’ll do

• Formalize mathematical content written in natural language into valid, compilable Lean 4 code
• Translate theorems, lemmas, propositions, and proofs into precise formal representations
• Ensure formal code accurately reflects the mathematical meaning and logical structure of the original statements
• Review and validate Lean 4 formalizations for correctness, consistency, and logical soundness
• Identify ambiguities, missing assumptions, or logical gaps in informal mathematical descriptions
• Contribute to high-quality datasets pairing human-written mathematics with formal Lean 4 equivalents for AI training

---

You’re a great fit if

• You have strong hands-on experience with Lean 4
• You have a solid background in mathematics, formal logic, or formal verification
• You are comfortable reading advanced mathematical texts and formalizing them accurately
• You write precise, correct, and maintainable Lean 4 code
• You have exceptional attention to detail and logical rigor
• You are interested in AI, automated reasoning, and mathematical verification

Bonus (not required):

• Experience with other theorem provers or formal systems
• Prior involvement in AI training, expert annotation, or reasoning-focused datasets
• Familiarity with research in proof assistants or formal methods

---

About the role

• Engagement: Contract (hourly)
• Hourly rate: $170-200 per hour based on performance and efficiency
• Location: Fully remote, work from anywhere
• Flexible workload: Set your own schedule
• High impact: Your work directly improves AI systems that reason about mathematics
• Growth potential: Top performers are selected for 3-month contracts and invited to advanced or leadership tracks

---

Getting Started: Step-by-Step (6 Minutes Total)

• Sign up here
• Enter your LinkedIn profile link (1 min)
• Verify your identity with Persona (a third-party verifier) (3 min)
• Access your dashboard and accept the paperwork (1 min)
• Link your Alignerr account to Hubstaff (1 min) [By clicking on "Create Hubstaff account"]

• Once you have completed the steps above, please send an email to alex@alignerr.com with the subject line “Lean 4” to help expedite the onboarding process.

  For more information, you can review these resources:

• Process Guide.

• FAQ page.

  ---

About Labelbox

Labelbox builds the data engine that accelerates breakthrough AI. Through its platform, expert services, and talent network (Alignerr), Labelbox enables leading research labs and enterprises to build safer, smarter models by iterating on data as effectively as they do on code.

[Junyan Xu]

I can't find any $200/hr Lean jobs searching on the platform:
image.png
(there are 124 jobs of the range $70-150/hr and look like a lot of duplicates (raises red flags))

The subreddit is quite active, but there's also a post claiming that the platform is a scam:

The majority of applicants will not receive actual job assignments. The company is utilizing candidates to train their AI interview system while collecting and monetizing personal data in the process.

[Alexander Pimentel Gomez]

Hi @Junyan Xu , the pay rate update was made last night. I’ve already requested the change to $170-200 USD, and it should be updated within a couple of hours.

About the post claiming that the platform is a scam, that information is not correct. All candidates who are accepted and complete work are paid for their contributions. Compensation is clearly defined before a project begins, and payments are processed exclusively through official platforms.

Candidates are removed from the platform only if they violate project or platform guidelines. In such cases, any approved work is always paid out before the account is closed.

Please keep in mind that, as with many companies operating at scale, online comments can vary and don’t always reflect internal processes or the day-to-day experience of contributors. What I can assure you is that the company follows clear guidelines, provides support to freelancers, and maintains structured channels to address questions or concerns promptly.

[Alexander Pimentel Gomez]

If you or other folks in the community have questions or if you want more information, please book a Zoom call directly with me [here]

[Jack McKoen]

I just got an email from "Alignerr" this morning advertising an "exclusive onboarding process" for this. Not sure how you got my email (it's technically in my CV on my website, but it's more likely you scraped it from somewhere if you're doing this at scale), but worse is that every link in the email was a tracking link, including the embedded images! Gross!

If you want my attention, send me an email I don't feel I have to sanitize

[Kim Morrison]

@Alexander Pimentel Gomez (this is with my Mathlib maintainer hat on): please respond promptly about these questions about spam emails. In particular, if you have in any way extracted emails from this Zulip, I would hope that you will apologise, and assure us that you have deleted them again.

[Alexander Pimentel Gomez]

Hi @Kim Morrison I want to reassure you that we have not extracted email addresses from this Zulip, nor do we have the ability or intention to do so. This is simply not something we do, and we take data privacy and community trust very seriously.

[Alexander Pimentel Gomez]

Hi @Jack McKoen , indeed, your email is publicly available on your website. Sorry if this caused any inconvenience. I’d just like to clarify that we do not scrape email addresses.

[Julian Berman]

Are you saying you're manually identifying people you're interested in and then trying to find their email addresses?

[Alexander Pimentel Gomez]

As a recruiter, I have to look for candidates who might be interested in an opportunity, and if they decide to move forward, they do need to verify their email address, as all companies do. @Julian Berman

[Jack McKoen]

If you go to all that effort of finding people and their emails (mine is not immediately visible, so you seem to be implying you were interested enough to dig around my website), why send such a generic (spammy) email?

[Julian Berman]

@Alexander Pimentel Gomez Sure, but I'm trying to understand what you mean by saying you're not scraping emails -- Jack (and myself, so I bet others) received emails from you, though we didn't share them with you -- just trying to make sure I understand the nuance in you saying you're not scraping them, is the differentiation you're making that you're not systematically automatically downloading emails but are doing so manually instead?

[Alexander Pimentel Gomez]

@Julian Berman Correct. Personally, I’ve been looking for people proficient in Lean 4 since early December. This is a very small and specialized community, and qualified candidates are genuinely hard to find. As part of that process, I sometimes reach out individually using publicly available contact information, without any automated or bulk collection.

[Alexander Pimentel Gomez]

@Jack McKoen That’s a fair point. The initial message was kept generic to avoid assumptions when reaching out cold, but I understand how it can come across as spammy given the context. That feedback is helpful, and I’ll take it into account going forward.

[Julian Berman]

Got it, thanks for clarifying. If it's done in the way you say, I don't personally have an issue then with the way you went about reaching out (though others still may clearly if they feel it's not welcome to do so without explicitly opting in).
EDIT: turns out that was a lie.

[Jack McKoen]

Alexander Pimentel Gomez said:

The initial message was kept generic to avoid assumptions when reaching out cold

And yet you assume I'm okay with all the tracking links! Can you comment on these? I think they completely destroy any good will

[Alexander Pimentel Gomez]

@Jack McKoen > The tracking links are part of our standard email tooling and are not intended to track individuals or behavior in a detailed way. I understand how they can feel intrusive, especially in a cold outreach context, and I appreciate you raising it. I’ll take this feedback back to the team and we can avoid using them in similar outreach going forward.

[Yan Yablonovskiy 🇺🇦]

This seems pretty shady to me , you seemingly mass emailed , I don’t see the criteria of it being some “targeted lean experts “ . You emailed me who is a complete beginner at lean , for example? And I saw on another thread someone was emailed who hadn't even used in Lean in a long time. What is the criteria you used to email?

[Kim Morrison]

@Yan Yablonovskiy 🇺🇦, I think that's a bit disingenuous. You've been active on the Lean zulip for over a year, I don't think you get to say "complete beginner" anymore. :-)

[Yan Yablonovskiy 🇺🇦]

I am very active on Zulip thats true, of note is that the email was sent to my email that exists only as my Zulip registration / github and is not used anywhere else ( the recruitment email is the only non-github / zulip email in the entire inbox ).

But @Jack McKoen says his email was a bit more effort to get, so perhaps it is true that it was not entirely scraping and this "recruiter" just really wants some leads.

[Kevin Buzzard]

To my surprise, my spam email was sent to my gmail account (which is not the email address I use here or indeed in most mathematical communications).

[Ilmārs Cīrulis]

Oh, there's a discussion about the email. (I got it too.)

I'm definitely underqualified for the 170-200$ per hour.

[Eric Wieser]

I see no explanation here other than that @Alexander Pimentel Gomez is scraping GitHub commits, since I received the email on an address that was coined for exactly one commit in a lean GitHub repo published by my employer

[Adam Topaz]

I can confirm that I also got this email at a custom address used a couple of time to make a mathlib commit, and for absolutely nothing else.

[Oliver Soeser]

The email I got was sent to a different address from the one I list on my website, github, etc. I don't see how you could find this address of mine without some kind of scraping (and if you truly are that interested in contacting me specifically, why send me an email where you don't even address me by name).

[Calvin Lee]

Scraping commits from github for these "job offers" also violates their acceptable use policy

[Calvin Lee]

The labelbox company appears to have a github which you can report for abuse here: https://github.com/labelbox

[Christian Krause]

Just as another datapoint: I also received an email on my email that i use for github and zulip, although my last mathlib commit is quite long ago.

[Andrew Peterson]

I got an email, but I've never made a commit to mathlib. I have not forked it either.

[Notification Bot]

This topic was moved here from #job postings > Lean 4 Mathematical Formalization Expert $170-200 by Johan Commelin.

[Johan Commelin]

I have moved this message out of #job postings.
I would have deleted this message, but I think it is useful to preserve the discussion that follows it.
With my Zulip admin hat on: We don't condone email scraping, and I'm sorry that this has happened.

[Ruben Van de Velde]

Ilmārs Cīrulis said:

Oh, there's a discussion about the email. (I got it too.)

I'm definitely underqualified for the 170-200$ per hour.

You might be surprised :)

[Ilmārs Cīrulis]

Ruben Van de Velde said:

You might be surprised :)

I doubt it. :) The best I can offer is formalizing human proofs of some math olympiad problems (using Mathlib) or something of similar difficulty that doesn't require contributing to Mathlib. :sweat_smile:

(I probably didn't get the joke. My apologies :sweat_smile:)

[Tainnor]

I also was contacted by email. My only mathlib contribution was fixing the spelling of "Weierstraß" in some comments.

Have to admit that it sounded tempting (would be amazing to get paid to write Lean, even though I suck at it), but it just seemed overall incredibly scammy, especially the whole application process.

[Rida Hamadani]

I also have received this spam.

@Tainnor since you found it tempting, I want to note that there are many other companies (who don't resort to spamming) that hire freelancers to do just that, I suggest going through the job posting channel.

[David Michael Roberts]

I got the email too and I know at most epsilon (for some epsilon << 1) about writing Lean 4. I have zero online that would indicate I have done anything with Lean myself, so it's presumably just someone who scraped this forum for email addresses.

[David Michael Roberts]

I haven't even made comments in here that would indicate I know anything about Lean, I'm just here for mathematical discussion.
On a pseudonymous social media account I reported on trying to vibe-code some lean and it failing badly, I hardly think that qualifies me to be approached. I am suspicious that whoever emailed me wasn't actually looking that hard to check if I actually fit the bill, so it sounds like some level of non-conscious action went into the process.

[Malvin Gattinger]

Just to add one more data point that this is not carefully manually sent special invitations but mass mailing spam: I received the mail twice, to slightly different email addresses and my working assumption is that they were obtained from git repo histories.

If you are so eager to get Lean experts and willing to pay for it, next time please already pay us for reading your emails. Should be easy to automate with all those tracking links ;-)

[Fabian Odermatt]

I feel left out, I didn't get an email. :(

[Nick Adfor]

Tainnor said:

I also was contacted by email. My only mathlib contribution was fixing the spelling of "Weierstraß" in some comments.

Have to admit that it sounded tempting (would be amazing to get paid to write Lean, even though I suck at it), but it just seemed overall incredibly scammy, especially the whole application process.

Oh, I've known how to get paid to write Lean

[Nick Adfor]

https://arxiv.org/abs/2511.02872
As you can see this FATE benchmark, the FATE-M benchmark (Textbook-level basic exercises) is generated by hiring first year student student and providing them accomodation (https://mp.weixin.qq.com/s/SZm4ikZGyOQteBr65ML2uw)

[Nick Adfor]

FATE-H benchmark (Problems at the level of honors course exams or graduate-level difficulty) is generated by Ubiquant (a quantitative firm) paying money for every exercise code and choosing 100 exercises from the code it gained. As you can see here Ubiquant is one of the writers https://www.selectdataset.com/dataset/fd2cdc49de9bf40ab7ca2db704fc189b

[Nick Adfor]

And FATE-X (Problems at the level of PhD qualifying exams or beyond) is generated by workshop at university, providing accomodation for the PhD student and Professors.

[Nick Adfor]

It can be seen as academic cooperation or company-university integration (here the company has endorsement from university), and can also be seen as blood diamond. In any case, it remains a way to make one's work stand out. Anyway, to send or not to send—both the sender and the recipient must be willing to engage.

[Scott Buckley]

@Nick Adfor I am deeply confused by that message. I read it through three times and I still don't know what you're talking about. Do you mean payment when you say accommodation? I didn't follow the links apart from the arXiv one, they seem a bit shady.

[Scott Buckley]

Anyway, I also got this spam message on LinkedIn. I reported it as spam.

[Nick Adfor]

Scott Buckley said:

I didn't follow the links apart from the arXiv one, they seem a bit shady.

These are Chinese websites so they seem a bit shady for you. But if you want to understand more about how the arxiv article generated (how to find enough personnel to practically implement the dataset, rather than just theoretically completing it mathematically), you can just translate it using Google.

[Nick Adfor]

Scott Buckley said:

Do you mean payment when you say accommodation?

It offers both payment and accommodation. The payment will be transferred directly to your bank account, while the accommodation provides free room and board on campus so that all participants can live, study, and work together. These two benefits are provided as part of hiring and training coders to write the benchmark code.

[Junyan Xu]

The job(s) advertised in this topic is fully remote though; and if it's in China $170-200/h is even more unlikely ...