Matthew Liu

Welcome

I’m a second-year undergraduate mathematics student at the University of Waterloo. Previously, as a high school student, I also took part in an eight-credit, undergraduate-level program at Harvard University.

I currently work as a research assistant for Dr. Jun Liu at the University of Waterloo. I lead the lab's work on the formal verification of mathematics using Lean, a functional programming language and theorem prover. It focuses on translating mathematical concepts, definitions, and proofs from natural language into a formal language that can be verified by a computer.

I am currently the 10th-ranked cuber in Canada for solving the Rubik's Cube in the Fewest Moves, with a result of 25 moves. My peak ranking was 10th in Canada, achieved in December 2025.

I am also a classically trained pianist, having earned my ARCT certification in 2024 from the Royal Conservatory of Music (RCM), a world-renowned music school based in Toronto, Ontario, Canada.

I am an ambitious, motivated, and hard-working individual with a diverse set of credentials and experiences. This website aims to capture my life, work, and way of thinking from both professional and personal perspectives.