Moving to AWS

Stream: general

[Leonardo de Moura]

After 17 years at Microsoft Research, I have decided to leave Microsoft. I am truly grateful for the invaluable support and opportunities that MSR has provided me over the years, allowing me to focus on my passion for exploring theorem provers and automated reasoning, and work on Lean full-time. It is rare to find a job that enables such a sustained and deep focus on a single area of research, and I feel fortunate to have had the chance to do so.

I am thrilled to share that I will join the Automated Reasoning Group at AWS tomorrow. This is an exciting new chapter in my career, and I look forward to working with both old and new friends and colleagues. I will continue leading the Lean project from there. It will take me a few months to settle on my new position, but I am excited about the future and expect to find new applications for Lean there.

[Matthew Ballard]

Congratulations! :tada:

[Jason Rute]

Congratulations! Is that the group John Harrison is part of?

[Leonardo de Moura]

Jason Rute said:

Congratulations! Is that the group John Harrison is part of?

Yes :)

[Jeremy Tan]

Who is John Harrison?

[Chris Hughes]

https://www.cl.cam.ac.uk/~jrh13/

[Siddharth Bhat]

An amazing researcher, who has implemented HOL light, done a huge amount of work on floating point verification (https://www.cl.cam.ac.uk/~jrh13/)

[Eric Wieser]

Based on John Harrison's page, does that mean relocating to Portland, or does the team have a presence alongside the rest of Amazon in Seattle?

[Leonardo de Moura]

Eric Wieser said:

Based on John Harrison's page, does that mean relocating to Portland, or does the team have a presence alongside the rest of Amazon in Seattle?

Nope. The Automated Reasoning Group is all over the place. I will stay in the Seattle Area. My manager is in New York :)

[Oisin McGuinness]

Siddharth Bhat said:

An amazing researcher, who has implemented HOL light, done a huge amount of work on floating point verification (https://www.cl.cam.ac.uk/~jrh13/)

John Harrison's talk at the recent IPAM conference Machine Assisted Proofs is highly recommended, (interesting history + formalization of isoperimetric theorem, slides included in link). Leo's talk on Lean also excellent. And several other great talks too!

[Junyan Xu]

YouTube link to the talk and workshop