Part-Time Lean4 Research Opportunity at ABAKA AI

Stream: job postings

[Heye Liu]

Part-Time AI Research Opportunity at ABAKA AI
ABAKA AI is a leading artificial intelligence company committed to becoming the data partner of the AI industry. We provide expert-level data engineering platforms and customized dataset solutions—including data collection, cleaning, and annotation—to top technology companies and research institutions worldwide.

We are seeking individuals with strong mathematics backgrounds and Lean 4 formalization experience to join a long-term collaboration on a cutting-edge AI research project.

Responsibilities

• Formalize IMO-level mathematics problems using Lean 4

• Ensure that formalizations are logically rigorous, clearly structured, and verifiable in Lean

• Work from provided Q&A pairs based on unformalized, competition-level math problems, and convert them into structured formal proofs

Qualifications

• Background in mathematics or a related field (undergraduate level or higher)

• Familiarity with category theory, type theory, or other abstract mathematical tools

• Proficiency in Lean 4, with the ability to independently complete formal verification of complex theorems (e.g., algebraic geometry, number theory)

• Prior experience in mathematics competitions (e.g., AMC, AIME, USAMO, Putnam, IMO)

Work Structure & Compensation

• Fully remote and part-time, with flexible hours and task-based assignments

• Competitive hourly rate, up to $100 USD, depending on qualifications and performance

If this opportunity aligns with your skills and interests, please send your resume to lhy@molardata.com. We will follow up with a trial task to help you get a better sense of the work involved.
Referrals and reposts are welcome!

[Ilmārs Cīrulis]

12 days and still no promised feedback on trial task solution.
That probably means that my solution was shockingly bad. :sweat_smile: