Online Part-time Annotation Opportunity at PKU

Stream: job postings

[Jiang Jiedong]

Online Part-time Annotation Opportunity: Abstract Algebra Lean Formalization at Peking University

We are excited to announce an online annotation opportunity with the Large Model Training Team at Peking University, focusing on Abstract Algebra Lean Formalization. This is a unique chance to contribute to cutting-edge research and enhance your skills in formal theorem proving.

What We Are Looking For:

• A strong background in abstract algebra and commutative algebra, as well as other undergraduate-level courses in algebra.
• Proficiency in using Lean4 for the formalization of mathematical theorems.
• Preference will be given to candidates with experience in formal proof projects or contributions to Mathlib.

Compensation:

• Payment is per problem, ranging from $20 to $60 USD per problem.
• Compensation will be sent the following month after the review and approval of the completed annotations.
• We offer customized payment arrangements to ensure convenient and timely compensation.

Why Join Us?

• Work with one of China's top higher education institutions. Peking University boasts a strong academic research background and abundant educational resources, providing solid support for the project.
• Contribute to a leading AI for mathematics project with significant scientific and social impact.
• Gain valuable experience in formal theorem proving and abstract algebra, while being part of a dynamic and innovative team.

How to Apply:
If you are interested, please send an email to peking.ai4math@gmail.com with your resume and a brief description of your relevant experience.