需要会lean4代码和熟悉Mathlib 定理库的人形式化数学题目，将数学题目的自然语言转化为lean4代码

Job ID: 39255714

Budget: $2 – $8 USD

我们会提供高中的数学题目，难度分为简单题和竞赛题目，需要人将题干部分使用lean4代码形式化出来，并保证可以通过编译

Related categories: Matlab and Mathematica Mathematics Engineering Mathematics