About me

I am a PhD student at the Cambridge Computer Laboratory, supervised by Professor Mateja Jamnik and Professor Wenda Li.

I also part-time at Mistral AI. I’m a contributor to Mistral-7B-v0.1.

I go by Albert. You can also call me 乔楚 (Qiaochu). (They look very different, but a name is nothing more than a lambda variable)

You can find my CV here.


I study how to learn abstract mathematical reasoning, with large (>20B) and small (<1B) language models.

  • I worked on the autoformalization of theorems and proofs.
  • I worked on integrating and improving premise selection tools with language models.
  • I study the interaction between humans and language models on mathematical tasks.
  • I am working on mathematical conjecturing. A foretaste of what I want to do here.

Here are some people I worked with/am working with closely on AI x Maths. You should consider reading their works if interested in the topic. In alphabet order:


Between July and October 2022, I was a research scientist intern at FAIR.

News and publications


qj213 AT cam DOT ac DOT uk

Random meetings

If you want to talk about AI4Maths, feel free to schedule a meeting: https://calendly.com/aqj. Please include your name and a meeting link if it’s virtual. Please send an email or a note explanation.

Resources for writing the PhD application research proposal

This section of Sharon Goldwater’s homepage.