Hi! My name is André Duarte and I’m currently a PhD researcher on automated theorem proving at the University of Manchester, under the supervision of Prof. Konstantin Korovin. I’m currently focused on efficient ways of dealing with specific hard theories, such as arithmetic or associative-commutative operators, while retaining full completeness and generality for arbitrary problems. My research has applications in domains where these theories are important, such as in formal verification of software, or in theorem proving for mathematics.

Previously I got my BSc and MSc in Physics from the University of Coimbra, with a specialisation in computational physics, having written my thesis on the internal composition of neutron stars.

Feel free to reach out to me with any questions!

Contact me

  • mail [ɑt] andrepd.me (preferred)
  • andre.duarte [ɑt] manchester.ac.uk

For encryption, feel free to use this key.

If you’d like to reach me in some other way, please email me and I’ll be glad to exchange some other method of contact.


Download my CV here.


See also my dblp and orcid pages.

Other stuff

  • quantum-tptp: Automated verification of quantum circuits.

  • ocaml-posit: A library for using Type III unums in OCaml. (WIP)

  • rprover: An automated theorem prover focusing on extensibility and speed, written in Rust.

  • LibriVox: My LibriVox contributions.