Emil Elakehal

Mathematics undergraduate at ETH Zürich.

"We can only see a short distance ahead, but we can see plenty there that needs to be done." Alan Turing

Currently exploring

I am still a student, learning all of this with a lot of curiosity and no claim to know much about it yet:

  • Formal methods and verification: Formal verification of software, cryptographic protocols and AI systems, automated theorem proving, proof assistants (Lean), type theory and the proofs-as-programs view (Curry-Howard).
  • Cryptography, privacy and security: Theoretical cryptography (foundations of cryptography, provable security), applied cryptography and protocols, privacy-enhancing technologies, zero-knowledge proofs, cryptographic obfuscation, post-quantum cryptography, secure and trusted hardware, cryptocurrencies and decentralized systems.
  • Formally verifying AI alignment and control: Specifying goals and values precisely, verified control and containment, provable safety guarantees and their limits, language and alignment.

Curious about

These I mostly study for personal satisfaction. See my AI views below for why I think they might come to matter more than that.

Foundations of mathematics and the limits of formal systems

  • What must we assume to do mathematics, and am I comfortable with it? (ZFC, first-order logic, formalism, platonism)
  • What are the consequences of incompleteness and undecidability in practice? (Gödel, Tarski's undefinability of truth, the Entscheidungsproblem)
  • What is the nature of the mathematics that formal systems can't capture? (continuum hypothesis, independence results)
  • How do we answer the skeptic when every justification, in mathematics and in the systems we trust, has to bottom out somewhere? (Münchhausen trilemma, coherentism, trusted computing base)
  • What are the ultimate limits of efficient computation, and does physical reality respect them? ((Extended) Church-Turing thesis, quantum computing)

Language, logic and reasoning

  • How does language shape the way we reason? (linguistic relativity, Wittgenstein)
  • Does symbolic logic describe how we actually think, or point at something platonic? (non-classical logics, logicism, intuitionism)

Determinism and the physical world

  • Does true randomness exist, or is the universe deterministic? (Bell's theorem, interpretations of quantum mechanics)
  • How does order emerge from randomness? (classical limit of QM, thermodynamic irreversibility, chaos theory)

Current views on AI

These are my speculative beliefs, and I always welcome a well-argued alternative.

  • Stance: AI is a genuinely transformative technology. I try to keep up with it and make decisions with AGI timelines in mind.
  • Not a luddite: Capability only moves one way. Cryptographic attacks only get stronger, and models only get smarter. Refusing the technology does not hold the line, it just leaves us behind it. If something is genuinely smarter, regressing ourselves to feel more human is the wrong response. Better to understand it and have a hand in how it gets integrated into society.
  • Mathematics: I expect mathematics and theoretical research to be transformed, with proving increasingly automated. When machines prove better than we do, the interesting human question shifts from how to formalize to what we want mathematics to be, understanding over formalism. That is why the questions above, which I pursue for satisfaction today, may become widely relevant.
  • Specification becomes the bottleneck: As AI takes over writing and optimizing code, the hard part is no longer the implementation but deciding what we actually want and stating it precisely. Formal verification only helps if we can capture our intentions, so I think software trends toward humans understanding what they want and expressing it accurately in a formal language. I expect formal verification to become a staple of software development and security.
  • My focus: I will probably spend my working life on applied, high-impact work, mainly formal verification and cryptography, as tools for integrating AI into society safely. These happen to line up with what I already enjoy, so I hold the reasoning loosely: all this predicting of what will stay important may just be me justifying the interests I already have. The deeper questions I mostly chase for personal satisfaction, and I think it is plausible that a greater intelligence will answer many of them sooner than I could, which is part of why getting its integration right feels more useful than chasing them head-on.
  • Safety: Both alignment and control work matter. I am personally more interested in the control side right now: tooling that keeps systems deterministic, sandboxed and formally verified under human specification. However I understand that formal verification has real limits and any system ultimately rests on assumptions it cannot itself prove.
  • My worries: I think the following are very real short term threats: mass surveillance, centralization / lock-in, increasing cyber-attacks, and gradual disempowerment. So I now put more effort into privacy, open source, censorship resistance, and self-hosting.
  • d/acc: A few pieces that resonate with me: Vitalik Buterin on formal verification, why privacy matters, and d/acc, which is roughly the approach to building technology I agree with. More broadly I am highly aligned with cypherpunk principles.

Connect

If any of this interests you, I would be grateful to hear from you. If you are in Zürich I am always glad to meet for lunch. If not, an email is welcome, maybe I'll have the chance to visit your city some day :)