APRIL | Minchao Wu

Tell us a bit about yourself?

I am a Ph.D. student in computer science at Australian National University, under the supervision of Michael Norrish. Before coming to ANU, I received an MS in Logic, Computation, and Methodology from Carnegie Mellon University, where I was advised by Jeremy Avigad. I am generally interested in logic, formal methods and automated reasoning. I am interested both in formalization and the development of tools for interactive theorem proving. In particular, I enjoy applying machine learning to improving high-level automation in ITP.

What gets you excited about your work/project?

The idea that a machine can learn to prove mathematical theorems intrigues me. I could imagine a future human and machine work together to solve open problems.

What are your top 3 professions?

1. Formal methods

2. Interactive theorem proving

3. Machine learning

What are your top 3 skills?

1. Programming

2. Problem solving

3. Logical thinking

How will your research change the world?

I hope that my research provides unique insights into autonomous approach to the discovery of mathematical knowledge.

What attracted you to apply for a scholarship with CSIRO’s Data61?

The well-known researchers affiliated with it and the computing resources.

Tell us about your CSIRO’s Data61 experience?

My Data61 supervisors are energetic and responsible. It is great experience working with them.

Why do you like working at CSIRO’s Data61?

Data61 provides me with sufficient computing resources I need for my research.

What have you discovered about CSIRO’s Data61 that you did not know?

There are positions called proof engineers.