Hi there! I'm mei, or Maja Kądziołka if you're all formal and uptight. I'm a queer weirdo who's into computers; currently an undergraduate student at the University of Warsaw. Also, I guess I get to call myself a researcher now? Feels weird.

While I find vast swathes of computer science interesting, lately my focus is mainly on things that involve symbolic manipulation in one way or another: compiler engineering, proof assistants, automatic theorem provers, static program analysis, and so on.

I've been known to have a soft spot in my heart for e-graphs — legend has it I'm always on the look out for reasons to use one.

Between classes at the university, I tend to either contribute to various open-source projects, such as the Rust compiler, or spend my time formalizing stuff in a proof assistant, mostly to learn mathematics better.

In the long term, I have two main goals:

• help push forwards the correctness guarantees we can make at the bedrock layers of computing, by building formally verified compilers, proof assistant kernels, operating systems, hypervisors, language runtimes, and hardware;
• improve the usability of proof assistants, to allow for their adoption by a wider group of professionals, make existing users more productive, as well as to allow creating particularly accessible learning materials for mathematics and computer science.