Jiazhi Chen
Hangzhou No.2 High School of Zhejiang Province
Education
Research
- Proved the exact values sat(6) = 30 and sat(7) = 55 using blocker reductions, finite classification, and explicit constructions.
- Formalized the complete proof in Lean 4 and released the source code, SAT certificates, and replay scripts.
- Archived the manuscript and reproducibility materials on Zenodo (DOI: 10.5281/zenodo.21770438).
Honors
Informatics Competitions
- NOIP – First Prize2025
- CSP-S – First Prize2025
- USACO – Platinum Division2026
Mathematics Competitions
- AIME II – Score: 11/152026
- AMC 12 – Distinction (Top 5%); 3rd Place at the Test Center2025
- AMC 8 – Perfect Score (25/25)2023
Other Honors
- Huilan Award, Hangzhou No.2 High School of Zhejiang Province2026
- Science and Innovation Star Award, Hangzhou No.2 High School of Zhejiang Province2025
- Desmos Studio Math Art Expo – Featured Artwork2024
- Chinese Weiqi Association – Amateur 5-dan2019
Technical Skills
- Languages
- C++, Python, TypeScript, JavaScript
- Formal Methods
- Lean 4, SAT solving, proof formalization
- Web Development
- React, Node.js, HTML/CSS, Docusaurus
- Tools
- Git, Linux, Docker, LaTeX, GitHub Actions
Research Interests
Combinatorics, Extremal Set Theory, Formal Verification, Algorithms