CV
Jingren Zhou (Jasper)
BSc (Hons) Mathematics, University of Edinburgh
Incoming MSc Student in Mathematics and Foundations of Computer Science, University of Oxford (2026–2027)
Location: United Kingdom
Email: pianoart@zhoujingren.com
GitHub: github.com/zhoujasper
Personal Website: zhoujasper.github.io
Profile
I am an incoming MSc student in Mathematics and Foundations of Computer Science at the University of Oxford, after completing my BSc (Hons) Mathematics at the University of Edinburgh. My academic background is primarily in rigorous proof-based mathematics, with strong results in algebra, commutative algebra, logic, analysis, complex variables, and numerical linear algebra.
My current research interests lie in the mathematical foundations of computation, especially formal verification, programming languages, proof assistants, type theory, and quantum computation. I am particularly interested in research areas where algebraic, logical, categorical, or type-theoretic structures provide rigorous guarantees about computation, correctness, and information.
I am preparing for research directions around formalised mathematics, program verification, type systems, theorem proving, verified algorithms, quantum processes, quantum programming languages, and quantum program reasoning. Alongside my pure mathematical background, I have completed computational projects in CP-SAT modelling, graph neural networks, statistical modelling, optimisation, and simulation.
Education
University of Oxford
MSc in Mathematics and Foundations of Computer Science
Incoming, 2026–2027
- Intended study areas include formal verification, programming languages, proof assistants, type theory, category-theoretic structures, quantum computation, and the mathematical foundations of computation.
- Particularly interested in courses and topics such as computer-aided formal verification, lambda calculus and types, categories, proofs and processes, quantum information, and quantum processes.
University of Edinburgh
BSc Mathematics with Honours
2023–2026
- Completed undergraduate study with First Class Honours-level performance.
- Entered directly into second year and achieved strong results across pure mathematics, computational mathematics, statistics, optimisation, and mathematical modelling.
- Final-year group project: Approximation by Rationals, supervised by Professor Jim Wright.
- Selected advanced modules include Commutative Algebra, Numerical Linear Algebra, Geometry, Mathematical Biology, Algebraic Geometry, Analytic Number Theory, Advanced Methods of Applied Mathematics, Topics in Applied Operational Research, and Incomplete Data Analysis.
Selected academic results
| Area | Selected courses and marks |
|---|---|
| Algebra, logic, and proof-based mathematics | Honours Algebra 97, Commutative Algebra 95, Fundamentals of Pure Mathematics 93, Logic 1 90, Geometry 85 |
| Analysis, complex variables, and differential equations | Several Variable Calculus and Differential Equations 95, Honours Complex Variables 94, Honours Differential Equations 93, Numerical Ordinary Differential Equations and Applications 86, Honours Analysis 84 |
| Computational, numerical, and applied mathematics | Computing and Numerics 92, Mathematical Biology 83, Numerical Linear Algebra 82 |
| Probability, statistics, and modelling | Statistics 84, Probability 82, Statistical Methodology 81 |
Pennon Education
A-Level Mathematics, Further Mathematics, and Physics
2022–2023
- Achieved A* in Mathematics, A* in Further Mathematics, and A* in Physics.
Kunming No. 1 High School
Senior Secondary Education, Science Track
2020–2023
- Completed a rigorous science-track curriculum in China.
- Developed early interests in mathematical problem solving through olympiad-style training and international mathematics competitions.
Research Interests
- Formal Verification and Proof Assistants: Lean, Coq/Rocq, Isabelle/HOL, formalised mathematics, program correctness, verified algorithms, theorem proving.
- Programming Languages and Type Theory: lambda calculus, type systems, operational semantics, program logics, proof/program correspondence, certified software.
- Quantum Computation and Quantum Information: quantum algorithms, quantum processes, quantum programming languages, categorical quantum mechanics, ZX-calculus, quantum program reasoning.
- Algebraic and Logical Methods in Computation: algebra, commutative algebra, logic, categorical structures, and mathematically grounded theoretical computer science.
Selected Projects
Approximation by Rationals
Year 4 Group Project, University of Edinburgh · Supervisor: Professor Jim Wright
2025–2026
- Developed a proof-based mathematical account of Diophantine approximation, centred on how real numbers can be approximated by rationals.
- Studied continued fractions, Liouville's theorem, Thue's theorem, and their connections with Pell equations, binary homogeneous polynomials, and Dirichlet's Unit Theorem.
- Strengthened skills in rigorous proof, mathematical exposition, literature organisation, and building a coherent logical narrative across number theory and algebra.
- This project motivates my interest in transferring proof-based mathematical training toward formalised mathematics, theorem proving, and mechanised reasoning.
Constraint Programming for Mathematics Timetabling
TAOR Final Project, University of Edinburgh · Team Leader
2026
- Led the development and analysis of a large-scale CP-SAT model for honours-level Mathematics timetabling at the University of Edinburgh.
- Modelled course scheduling, student choice structures, fixed outside-school timetables for joint-degree students, clash feasibility, and timetable-quality rules.
- Used Google OR-Tools CP-SAT with student-type aggregation to reduce model size while preserving key combinatorial and programme-level structures.
- The project strengthened my interest in formal modelling, computational guarantees, and the gap between practical constraint systems and rigorous correctness/verification questions.
Random-Walk-Based Graph Neural Networks
Vacation Research Project
Summer 2025
- Investigated whether random-walk-based graph neural network methods can improve expressivity compared with standard message-passing GNNs.
- Studied limitations such as oversmoothing and oversquashing, and reviewed architectures including graph convolutional and graph attention networks.
- Explored theoretically motivated random-walk schemes and considered extensions to hypergraphs, where higher-order relationships cannot be fully captured by ordinary graph structures.
- Developed research skills at the intersection of graph theory, machine learning, representation learning, and mathematical modelling.
Quantitative Modelling of Winter Peak Electricity Demand in Great Britain
Statistical Modelling Project · Team Leader
April–May 2025
- Led a team project modelling winter peak electricity demand in Great Britain using historical data from 1991 to 2014.
- Built a multi-factor linear regression framework incorporating renewable generation, seasonal structure, and weekday effects.
- Designed an automated model-selection workflow using five-fold cross-validation, AIC, and BIC.
- Strengthened experience in reproducible modelling, validation, and communicating mathematical results from data.
BoxCar Ride-Sharing Simulation Study
Data-Driven Discrete-Event Simulation Project · Team Leader
February 2026
- Built a discrete-event simulation model of a ride-sharing system, capturing rider arrivals, driver availability, matching, trip execution, cancellations, revenue, and costs.
- Re-estimated key parameters using maximum likelihood methods and compared adjusted and original baselines.
- Analysed trade-offs between rider service quality, driver earnings, profitability, and system balance.
Strategic Workforce Allocation Optimisation
Optimisation Modelling Project · Team Leader
April 2025
- Formulated and solved a workforce allocation problem for a consulting firm using linear/integer optimisation.
- Used Xpress to evaluate scenarios involving role restrictions, transport disruption, remote-work limits, outsourcing, and demand variability.
- Developed experience in mathematical programming, structured modelling, and computational experimentation.
Multi-Stage Laptop Manufacturing System Simulation Study
Manufacturing System Simulation Project · Team Leader
April 2026
- Developed a Simul8 discrete-event simulation of a multi-stage laptop manufacturing system with blocking, rework, inventory control, component matching, and order-level synchronisation.
- Conducted input analysis using AIC, BIC, Kolmogorov–Smirnov testing, and maximum likelihood estimation.
- Diagnosed system bottlenecks and designed progressive improvement experiments.
Teaching, Leadership, and Representation
MathPALS Leader
Edinburgh University Students' Association / School of Mathematics, University of Edinburgh
April 2024–Present
- Led informal peer-assisted learning sessions for first-year Mathematics students in a supportive small-group environment.
- Helped students discuss core course questions, understand abstract mathematical ideas, and develop confidence in problem solving.
- Practised guiding discussion without simply giving away solutions and coordinated session preparation with other student leaders.
Student Representative
Edinburgh University Students' Association / School of Mathematics, University of Edinburgh
September 2024–June 2025
- Represented Mathematics students by collecting feedback on teaching, assessment, workload, resources, and academic experience.
- Communicated student concerns and suggestions through representative channels and staff-student liaison mechanisms.
- Developed communication, coordination, and problem-solving skills by translating student feedback into constructive recommendations.
Student Volunteer
Edinburgh University Students' Association / Saltire Awards
2025
- Completed at least 25 hours of volunteering and received the Saltire Awards “The Approach” certificate.
Volunteer / Outstanding Volunteer
Yunnan Nationalities Museum, Kunming, China
2021–2023
- Volunteered in public-facing museum cultural service and helped support the communication of Yunnan's multi-ethnic cultural heritage.
- Recognised as an Outstanding Volunteer for strong performance in volunteering activities.
Awards and Distinctions
- United Kingdom Best Pairs Entry, Simon Marais Mathematics Competition, 2025. Highest-scoring UK pairs entry in the West Division, achieved with Kevin Zhao.
- Top 3 in Programme / Top 5% in Year Group, School of Mathematics, University of Edinburgh, 2025. Ranked 3rd out of 24 in programme and 4th out of 120 in year group for 2024/25.
- Kelland Memorial Prize, University of Edinburgh, 2024. Awarded for distinguished performance as a direct entrant into second-year Mathematics.
- William and Isabella Dick Prize, University of Edinburgh, 2024. Awarded for outstanding performance in second-year Mathematics.
- School of Mathematics Vacation Scholarship, University of Edinburgh, 2024. Awarded summer research funding for supervised vacation research in mathematics.
- Top 25% Worldwide, Euclid Mathematics Contest, 2023. Certificate of Distinction in the University of Waterloo CEMC Euclid Contest.
- Third Prize, China Mathematical Olympiad, Provincial Level, 2021.
Technical Skills
Mathematics and theoretical preparation
Rigorous proof writing, mathematical exposition, algebra, commutative algebra, logic, analysis, numerical linear algebra, optimisation modelling, statistical modelling, simulation, and validation.
Programming and computational tools
Python, NumPy, Pandas, Matplotlib, PyTorch, R, Google OR-Tools CP-SAT, Xpress, Simul8, Excel VBA.
Developing research tools and interests
Lean 4, Coq/Rocq, Isabelle/HOL, SAT/SMT solving, Z3, theorem proving, quantum programming and verification tools.
Academic and professional tools
LaTeX, Overleaf, Git, GitHub, Microsoft Word, Excel, PowerPoint, Adobe Photoshop.
Languages
Chinese: native.
English: fluent.
Additional Interests
- Piano, with Level 10 certificate.
- Reading, photography, Sudoku, and badminton.
References
Available upon request.