昵称登录后显示

项目名称：数学竞赛题目形式化验证实践项目
项目描述：基于 Lean4 与 Mathlib 标准库，针对高中及大学阶段数学竞赛中的代数、数论与组合类题目开展形式化编码工作，将自然语言描述的解题思路与证明过程，转化为可被机器严格校验的定理证明代码，实现数学证明的可验证与可复现。
个人职责：独立完成 10+ 道典型竞赛题目的形式化建模与证明，熟练运用 linarith、nlinarith、induction 等核心 tactics 策略构建严谨的证明链条，调试并优化代码结构以提升可读性与验证效率，确保所有证明均通过 Lean4 编译器的严格检查，积累了丰富的形式化验证实战经验，具备独立承接相关任务的能力。