陈家治
浙江省杭州第二中学
教育经历
研究经历
- 通过阻断集归约、有限分类与显式构造，证明 sat(6) = 30 与 sat(7) = 55。
- 使用 Lean 4 形式化完整证明，并公开源代码、SAT 证书与重放脚本。
- 将论文与可复现材料存档至 Zenodo（DOI：10.5281/zenodo.21770438）。
荣誉奖项
信息学竞赛
- 全国青少年信息学奥林匹克联赛 一等奖2025 年
- CCF 非专业级软件能力认证提高级 一等奖2025 年
- 美国计算机奥林匹克竞赛 白金组2026 年
数学竞赛
- 美国数学邀请赛 II 11/15 分2026 年
- 美国数学竞赛 12 全球前 5%、考点第三名2025 年
- 美国数学竞赛 8 满分奖2023 年
其他荣誉
- 浙江省杭州第二中学“蕙兰奖”2026 年
- 浙江省杭州第二中学“科创之星”2025 年
- Desmos 数学艺术博览会 入选作品2024 年
- 中国围棋协会 业余 5 段2019 年
技术技能
- 编程语言
- C++、Python、TypeScript、JavaScript
- 形式化方法
- Lean 4、SAT 求解、证明形式化
- 网页开发
- React、Node.js、HTML/CSS、Docusaurus
- 工具
- Git、Linux、Docker、LaTeX、GitHub Actions
研究方向
组合数学、极值集合论、形式化验证、算法