Social
Automated reasoning

How the Lean language brings math to coding and coding to math

Uses of the functional programming language include formal mathematics, software and hardware verification, AI for math and code synthesis, and math and computer science education.

By Leo de Moura
August 16, 2024
12 min read
Share

This post is an adaptation of a keynote address that Leo de Moura delivered at the International Conference on Computer Aided Verification (CAV), in July 2024.

LEAN logo.png
The Lean logo.

In 2013, I launched the Lean project with the goal of bridging the gap between automated and interactive theorem provers. Since its inception, Lean has seen unparalleled adoption in the mathematical community, surpassing previous efforts in formalized mathematics. Lean 4, the latest version, is implemented in Lean itself and is also a fully fledged, extensible programming language with robust IDE support, package management, and a thriving ecosystem.

In 2023, Sebasian Ullrich and I founded the Lean Focused Research Organization (FRO), a nonprofit dedicated to advancing Lean and supporting its community. The Lean project embraces a philosophy that promotes decentralized innovation, empowering a diverse community of researchers, developers, and enthusiasts to collaboratively push the boundaries of mathematical practice and software development. In this blog post, we will provide a brief introduction to the project and describe how it is used at AWS.

A brief introduction to Lean

Lean is an open-source, extensible, functional programming language and interactive theorem prover that makes writing correct and maintainable code easy. Lean programming primarily involves defining types and functions, allowing users to focus on the problem domain and its data rather than on coding details. Lean has four primary use cases: formal mathematics, software and hardware verification, AI for math and code synthesis, and math and computer science education.

Formal mathematics

Lean allows mathematicians to work with advanced mathematical structures using syntax that feels natural to them. The math community recognizes its usefulness: for instance, Fields medalists Peter Scholze and Terence Tao used Lean to confirm their new results; Quanta Magazine has lauded Lean as one of the biggest breakthroughs in mathematics, and it has been featured in numerous popular scientific and academic publications, including the Wired magazine article “The effort to build the mathematical library of the future”. Recently, DeepMind used Lean to build an AI engine that met the silver-medal standard at the International Math Olympiad.

As of July 2024, the Lean Mathematical Library has received contributions from over 300 mathematicians and contains 1.58 million lines of code, surpassing other formal-mathematics systems in use. This remarkable growth has come despite Lean’s concision and youth: it’s at least a decade younger than comparable libraries.

Software and hardware verification

Lean’s combination of formal verification, user interaction, and mathematical rigor makes it invaluable for both software and hardware verification. Lean is a system for programming your proofs and proving your programs. An additional benefit is that Lean produces efficient code, and its extensibility features, originally designed for mathematicians, are also highly convenient for creating abstractions when writing clean and maintainable code. Its benefits extend to any system requiring exceptional accuracy and security, including industries such as aerospace, cryptography, web services, autonomous vehicles, biomedical systems, and medical devices. Later on, we will provide several examples of Lean's applications at AWS.

AI for math and code synthesis

Lean is popular with groups developing AI for mathematics and code synthesis. One of the key reasons is that Lean formal proofs are machine checkable and can be independently audited by external proof checkers. Additionally, Lean's extensibility allows users to peer into the system internals, including data structures for representing proofs and code. This capability is also used to automatically generate animations from Lean proofs.

AI researchers are leveraging large language models (LLMs) to create Lean formal proofs and automatically translate prose into formalized mathematics. OpenAI has released lean-gym, a reinforcement learning environment based on Lean. Harmonic used Lean in the development of its Mathematical Superintelligence Platform (MSI), an AI model designed to guarantee accuracy and avoid hallucinations. Meta AI created an AI model that has solved 10 International Mathematical Olympiad problems, and DeepMind has formalized a theoretical result related to AI safety in Lean. Additionally, LeanDojo is an open-source project using LLMs to automate proof construction in Lean.

Lean's unique combination of machine-checkable proofs, system introspection, and extensibility makes it an ideal tool for advancing AI research in mathematics and code synthesis. The synergy between LLMs and Lean formal proofs is emphasized in Terence Tao's colloquium lecture at the American Mathematical Society, “Machine Assisted Proof”; in the Scientific American article “AI will become mathematicians' co-pilot”; and in the New York Times article “A.I. Is coming for mathematics, too.”

Math and CS education

Millions of people learn mathematics as students and use it throughout their careers. Since its inception, the Lean project has supported students' mathematical-reasoning needs and enabled a more diverse population to contribute to the fields of math and computer science. Numerous educational resources are available for learning Lean, including interactive computer games such as the Natural Number Game, computer science and mathematics textbooks, university courses, and on-demand tutorials. The Lean FRO is committed to expanding Lean’s educational content and envisions a future where children use Lean as a playground for learning mathematics, progressing at their own paces and receiving instantaneous feedback, similar to how many have learned to code.

A quick tour of Lean

Lean combines programming and formal verification. Let's take a quick tour through a small example to see how we write code in Lean and prove properties about that code.

Writing code in Lean

First, let's define a simple function that appends two lists:

def append (xs ys : List a) : List a :=
  match xs with
  | [] => ys
  | x :: xs => x :: append xs ys

This function is defined using pattern matching. For the base case, appending an empty list [] to ys results in ys. The notation x :: xs represents a list with head x and tail xs. For the recursive case, appending x :: xs to ys results in x :: append xs ys. Additionally, the append function is polymorphic, meaning it works with lists of any type a.

Extensible syntax

The notation x :: xs used above is not built into Lean but is defined using the infixr command:

infixr:67 " :: " => List.cons

The infixr command defines a new infix operator x :: xs, denoting List.cons x xs. This command is actually a macro implemented using Lean's hygienic macro system. Lean's extensible syntax allows users to define their own domain-specific languages. For example, Verso, the Lean documentation-authoring system, is implemented in Lean using this mechanism. Verso defines alternative concrete syntaxes that closely resemble Markdown and HTML.

Proving properties about code

Next, we'll prove a property about our append function: that the length of the appended lists is the sum of their lengths.

theorem append_length (xs ys : List a)
        : (append xs ys).length = xs.length + ys.length := by
  induction xs with
  | nil => simp [append]
  | cons x xs ih => simp [append, ih]; omega

Here, theorem introduces a new theorem named append_length. The statement (append xs ys).length = xs.length + ys.length is what we want to prove. The by ... block contains the proof. In this proof,

  • induction xs with initiates a proof by induction on xs;
  • the nil case proves the base case using simp, the Lean simplifier. The parameter append instructs the simplifier to expand append’s definition; and
  • the cons x xs ih case proves the inductive step where ih is the inductive hypothesis. It also uses simp and omega, which complete the proof using arithmetical reasoning.

In this proof, induction, simp, and omega are tactics. Tactics, which transform one state of the proof into another, are key to interactive theorem proving in Lean. Users can inspect the states of their proofs using the Lean InfoView, a panel in the IDE. The InfoView is an interactive object that can be inspected and browsed by the user. In the following picture, we see the state of our proof before the simp tactic at line 10. Note that the proof state contains all hypotheses and the goal (append (x :: xs) ys).length = (x :: xs).length + ys.length, which remains to be proved.

LEAN example.png
The state of the proof before the simp tactic at line 10, as visualized in the Lean InfoView.

How Lean is used at AWS

At AWS, Lean is used in several open-source projects to address complex verification and modeling challenges. These projects not only highlight the practical applications of Lean in different domains but also emphasize AWS's commitment to open-source development and collaboration. We cover four key projects: Cedar, LNSym, and SampCert, whose Lean source code is already available on GitHub, and AILean, which is exploring the relationship between LLMs and formal mathematics and whose code is not open source yet. 

Cedar: an open-source policy language and evaluation engine 

Cedar is an open-source policy language and evaluation engine. Cedar enables developers to express fine-grained permissions as easy-to-understand policies enforced in their applications and to decouple access control from application logic. Cedar supports common authorization models such as role-based access control and attribute-based access control. It is the first policy language built from the ground up to be verified formally using automated reasoning and tested rigorously using differential random testing.

The Cedar project uses Lean to create an executable formal model of each core component of the Cedar runtime (such as the authorization engine) and static-analysis tools (such as the type checker). This model serves as a highly readable specification, allowing the team to prove key correctness properties using Lean.

Lean was chosen for modeling Cedar due to its fast runtime, extensive libraries, IDE support, and small trusted computing base (TCB). The fast runtime enables efficient differential testing of Cedar models. The libraries provide reusable verified data structures and tactics built by the open-source community. Lean’s small TCB allows Cedar to leverage these contributions confidently, as Lean checks their correctness, requiring trust only in Lean’s minimal proof-checking kernel.

LNSym: Symbolic simulation for cryptographic verification

LNSym is a symbolic simulator for Armv8 native-code programs. It’s currently under development, with a focus on enabling automated reasoning of cryptographic machine-code programs. Many cryptographic routines are written in assembly to optimize performance and security on the underlying processor. LNSym aims to reduce the cost of verifying cryptographic routines, particularly block ciphers and secure hashes, ultimately empowering cryptography developers to formally reason about their native-code programs.

LNSym uses Lean as a specification language to model the Arm instruction semantics and cryptographic protocols and as a theorem prover for reasoning about these artifacts. Since Lean programs are executable, the specifications achieve a high degree of trust through thorough conformance testing. Lean orchestrates proofs such that the heavy and often tedious lifting is done automatically, using decision procedures like SAT solvers or custom domain-specific tactics. When proof automation fails, users can employ Lean as an interactive theorem prover. This combination of interactive and automated theorem proving ensures that progress on verification tasks is not hindered by the limitations of proof automation.

SampCert: formally verified differential-privacy primitives

SampCert is an open-source library of formally verified differential-privacy primitives used by the AWS Clean Rooms Differential Privacy service for its fast and sound sampling algorithms. Using Lean, SampCert provides the only verified implementation of the discrete Gaussian sampler and the primitives of zero concentrated differential privacy.

Although SampCert focuses on software, its verification relies heavily on Mathlib, the Lean Mathematical Library. The verification of code addressing practical problems in data privacy depends on the formalization of mathematical concepts from Fourier analysis to number theory and topology.

AILean: AI for math and math for AI

AILean is exploring the relationship between LLMs and formal mathematics in collaboration with the Technology Innovation Institute (TII). This exploration works in both directions: AI for math and math for AI. In AILean, LLMs are used to enhance proof automation and user experience in formal mathematics. LLMs can analyze theorem statements and existing proof steps, suggesting relevant lemmas, definitions, or tactics to guide users in completing proofs. They can also identify common mistakes or inconsistencies, proposing corrections or alternative approaches that avoid dead ends and thereby improving the proof development process.

Takeaways

Lean is a complex system, but its correctness relies only on a small trusted kernel. Moreover, all proofs and definitions can be exported and independently audited and checked. This is a crucial feature for both the mathematical and software verification communities because it eliminates the trust bottleneck. It doesn't matter who you are; if Lean checked your proof, the whole world can build on top of it. This enables large groups of mathematicians who have never met to collaborate and work together. Additionally, it allows users to extend Lean without fearing the introduction of soundness bugs that could compromise the logical consistency of the system.

Lean's extensibility enables customization, which was particularly important during its first ten years, when resources were limited. Lean’s extensibility allowed the community to extend the system without needing to synchronize with its developers. Self-hosting, or implementing Lean in Lean, also ensured that users can access all parts of the system without having to learn a different programming language. This makes it easy and convenient to extend Lean. Packages such as ProofWidgets and SciLean are excellent examples of user-defined extensions that leverage these features.

The FRO model introduced by Convergent Research has been instrumental in supporting Lean and helping it transition to a self-sufficient foundation. The Lean project has grown significantly, and driving it forward would have been difficult without Convergent Research’s efforts to secure philanthropic support. Just as foundations like the Rust and Linux Foundations are vital for the success and sustainability of open-source projects, the support of Convergent Research has been critical for Lean's ongoing progress.

To learn more about Lean, visit the website.

Research areas
Tags
About the Author
Leo de Moura
Leo de Moura is a senior principal applied scientist with Amazon's Automated Reasoning group.

Related content

Work with us

See more jobs See more jobs
Senior Applied Scientist, Annapurna ML
US, WA, Seattle
The Annapurna ML team is looking for a Senior Applied Scientist to work on the intersection of Artificial Intelligence and program analysis to raise the code quality bar in our state-of-the-art deep learning compiler stack. This stack is designed to optimize application models across diverse domains, including Large Language and Vision, originating from leading frameworks such as PyTorch, TensorFlow, and JAX. Your role will involve working closely with our custom-built Machine Learning accelerators, Inferentia and Trainium, which represent the forefront of Annapurna innovation for advanced ML capabilities, and is the underpinning of Generative AI. As a Senior Applied Scientist, you'll be instrumental in designing, developing, and deploying analyzers for ML compiler stages and compiler IRs. You will architect and implement business-critical tooling, publish research, and mentor a brilliant team of experienced scientists and engineers. You will need to be technically capable, credible, and curious in your own right as a trusted scientist, innovating on behalf of our customers. Your responsibilities will involve tackling crucial challenges alongside a talented engineering team, contributing to leading-edge design and research in compiler technology and deep-learning systems software. Strong experience in programming languages, compilers, program analyzers, and program synthesis engines will be a benefit in this role. A background in machine learning and AI accelerators is preferred but not required. A day in the life Diverse Experiences Amazon values diverse experiences. Even if you do not meet all of the qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Why Amazon? We pioneered cloud computing and never stopped innovating — that’s why customers from the most successful startups to Global 500 companies trust our robust suite of products and services to power their businesses. Inclusive Team Culture Here at Amazon, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (diversity) conferences, inspire us to never stop embracing our uniqueness. Mentorship & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, mentorship and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why we strive for flexibility as part of our working culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve in the cloud.
Senior Applied Scientist, Perimeter Protection Applied Science
US, WA, Seattle
Join the AWS Perimeter Protection team as a Senior Applied Scientist, where you will bring your deep ML engineering expertise to design, build, and scale AI-driven security solutions that protect AWS customers worldwide. This role is ideal for someone who has already built and shipped production ML systems at industry scale and is looking to apply that experience to high-impact security challenges. You will own the full ML lifecycle — from research and prototyping to production deployment and optimization — powering services including Web Application Firewall, DDoS Protection, Bot Management, and Infrastructure Protection. With services spanning all AWS regions and handling trillions of requests per week, you will solve complex engineering and science problems where model performance, system reliability, and low-latency inference are critical. Key job responsibilities - Design, build, and deploy production-grade ML models and systems for real-time threat detection, mitigation, and protection against evolving cyber threats at cloud scale. - Own the full ML lifecycle end-to-end — from problem formulation, data engineering, and model development through to production deployment, monitoring, and continuous improvement. - Architect and optimize ML pipelines, training infrastructure, and serving systems to meet strict latency, throughput, and reliability requirements at AWS scale. - Bridge the gap between research and production by translating novel ML approaches into robust, scalable, and maintainable systems that operate in real-time security environments. - Design and implement feature engineering workflows and large-scale data processing pipelines to support rapid experimentation and reliable model iteration. - Collaborate closely with software engineering teams to integrate ML models into distributed, low-latency security services, driving engineering decisions around model serving, infrastructure, and system design. - Analyze large-scale production data to identify patterns, anomalies, and emerging threat vectors, and translate findings into measurable improvements to detection and mitigation capabilities. - Establish and improve best practices for ML system design, model evaluation, A/B testing, and production monitoring across the team. - Mentor junior scientists and engineers, raising the bar on both scientific rigor and engineering quality.
Applied Scientist, Neuron ARG, Annapurna ML
US, WA, Seattle
The Automated Reasoning Group in the Amazon Neuron team is looking for an Applied Scientist to work on the intersection of Artificial Intelligence and program analysis to raise the code quality bar in our state-of-the-art deep learning compiler stack. This stack is designed to optimize application models across diverse domains, including Large Language and Vision, originating from leading frameworks such as PyTorch and JAX. Your role will involve working closely with our custom-built Machine Learning accelerator, Trainium, which represents the forefront of innovation for advanced ML capabilities, and is the underpinning of Generative AI. In this role as an Applied Scientist, you'll be instrumental in designing, developing, and deploying analyzers for ML compiler stages and compiler IRs. You will architect and implement business-critical tooling, publish research, and mentor a brilliant team of experienced scientists and engineers. You will need to be technically capable, credible, and curious in your own right as a trusted AWS Neuron engineer, innovating on behalf of our customers. Your responsibilities will involve tackling crucial challenges alongside a talented engineering team, contributing to leading-edge design and research in compiler technology and deep-learning systems software. Strong experience in programming languages, compilers, program analyzers, theorem provers, and program synthesis engines will be a benefit in this role. A background in machine learning and AI accelerators is preferred but not required.
Applied Scientist, Delivery Networks and Tech
IN, KA, Bengaluru
Customer addresses, Geospatial information and Road-network play a crucial role in Amazon Logistics' Delivery Planning systems. We own exciting science problems in the areas of Address Normalization, Geocode learning, Maps learning, Time estimations including route-time, delivery-time, transit-time predictions which are key inputs in delivery planning. As part of the Science team within DNT (Last Mile), you will partner closely with other scientists and engineers in a collegial environment to develop enterprise ML solutions with a clear path to business impact. The setting also gives you an opportunity to think about a complex large-scale problem for multiple years and building increasingly sophisticated solutions year over year. In the process there will be opportunity to innovate, explore SOTA and publish the research in internal and external ML conferences. Successful candidates will have deep knowledge of competing machine learning methods for large scale predictive modelling, natural language processing, semi-supervised & graph based learning. We also look for the experience to graduate prototype models to production and the communication skills to explain complex technical approaches to the stakeholders of varied technical expertise. Here is a glimpse of the problem spaces and technologies that we deal with on a regular basis: 1. De-duping and organizing addresses into hierarchy while handling noisy, inconsistent, localized and multi-lingual user inputs. We do this at the scale of millions of customers for established (US, EU) as well as emerging geographies (IN, MX). We make use of technologies like LLMs, Weak supervision, Graph-based clustering & Entity matching. We also use additional modalities such as building outlines in maps, street view images and 3P datasets, gazetteers. 2. Build a generic ML framework which leverages relationship between places to improve delivery experience by learning precise delivery locations and propagating attributes, such as business hours and safe places. 3. (Work done in sister teams) Developing systems to consume inputs from areal imagery and optimize our maps to enable efficient delivery planning. Also building models to estimate travel time, turn costs, optimal route and defect propensities. Key job responsibilities As an Applied Scientist I, your responsibility will be to deliver on a well defined but complex business problem, explore SOTA technologies including GenAI and customize the large models as suitable for the application. Your job will be to work on a end-to-end business problem from design to experimentation and implementation. There is also an opportunity to work on open ended ML directions within the space and publish the work in prestigious ML conferences. About the team Last Mile Address Intelligence (LMAI) team owns WW charter for address and location learning solutions which are crucial for efficient Last Mile delivery planning. The team works out of Hyderabad and Bangalore offices in India. LMAI is a part of the DNT Science team, which also owns problems in the space of maps learning and travel time estimations. The rest of the DNT Science team and senior leadership of Last Mile org works out of Bellevue office.
Research Science Manager, Safe Autonomy, SAF Lab
US, CA, Pasadena
We are seeking a Research Science Manager to join the SAF Lab. In this role, you will lead a team of world-class applied scientists, engineers, post-docs and interns developing the next generation of safe autonomy on highly dynamic robotic systems. You will drive technical vision, research strategy, and ensure your team's innovations translate into production systems that operate at Amazon scale. You will interface with top academic researchers at the forefront of safe autonomy, and interdisciplinary teams across Amazon working on autonomous mobile robots, mobile manipulators, and dynamically stable robots. You will bridge academic research with real-world deployable safety layers that enable robots to safely operate around humans. Key job responsibilities • Manage a team of scientists and engineers developing a universal safety layer for robotic systems, with a focus on the next generation of robots • Work with leadership to design and execute multi-year research roadmaps for the development of safe autonomy that spans all types of current and emerging robotic platforms • Lead Scientists, Engineers, post-docs and interns to realize research and development goals and provide evidence of these results in a variety of formats • Drive integration of control barrier functions with planning, perception and learning while maintaining guarantees of safe high-performance robot behavior • Collaborate with product teams and science leaders to set a science roadmap (with eventual impact on real robots). • Publish research findings at top-tier conferences and contribute to the broader robotics community • Build relationships with academic and industry partners to stay at the forefront of safe autonomy A day in the life Amazon offers a full range of benefits that support you and eligible family members, including domestic partners and their children. Benefits can vary by location, the number of regularly scheduled hours you work, length of employment, and job status such as seasonal or temporary employment. The benefits that generally apply to regular, full-time employees include: 1. Medical, Dental, and Vision Coverage 2. Maternity and Parental Leave Options 3. Paid Time Off (PTO) 4. 401(k) Plan If you are not sure that every qualification on the list above describes you exactly, we'd still love to hear from you! At Amazon, we value people with unique backgrounds, experiences, and skillsets. If you’re passionate about this role and want to make an impact on a global scale, please apply! About the team Work with the inventor of control barrier functions in the Safe Autonomy Frontiers (SAF) Lab. The first industry research lab in safe autonomy, developing a universal safety layer for the next generation of robotic systems: mobile robots, manipulators, mobile manipulators, and future platforms with dynamic stability. You will push the frontiers of performant safety for highly dynamic robots: CBF theory integrated with perception and learning, evaluated on next-generation robots. Your work will underpin robots operating alongside people at Amazon's unprecedented scale.
Research Scientist II, Global Logistics, Applied Science Team
US, WA, Bellevue
Transform global logistics by developing innovative technological solutions that optimize complex international shipping networks. Join a dynamic team where your advanced scientific expertise will directly impact millions of packages moving across borders, solving intricate transportation challenges through applied science. Key job responsibilities - Develop advanced deep learning and generative AI applications for sophisticated product classification systems - Lead complex modeling analyses to support strategic business decision-making and policy development - Partner with engineering and operations teams to design transformative machine learning solutions for transportation challenges - Design and document technical strategies and applied science roadmaps - Innovate and provide technological direction in international imports and exports logistics A day in the life Your workday will be an exciting blend of data exploration, innovative problem-solving, and collaborative technology development. You'll dive into complex datasets, design sophisticated machine learning models, engage with cross-functional teams, and create technological solutions that reshape international shipping capabilities. About the team We are a passionate group of scientists and engineers dedicated to building comprehensive transportation technologies. Our mission is to create highly scalable, intelligent systems that enable seamless international package movement. By pushing technological boundaries, we're reimagining global logistics through innovative applied science. Amazon offers a full range of benefits that support you and eligible family members, including domestic partners and their children. Benefits can vary by location, the number of regularly scheduled hours you work, length of employment, and job status such as seasonal or temporary employment. The benefits that generally apply to regular, full-time employees include: 1. Medical, Dental, and Vision Coverage 2. Maternity and Parental Leave Options 3. Paid Time Off (PTO) 4. 401(k) Plan Learn more about our benefits here: https://www.amazon.jobs/en/internal/benefits/us-benefits-and-stock
Applied Scientist II, Special Projects
US, WA, Seattle
Innovators wanted! Are you an entrepreneur? A builder? A dreamer? This role is part of an Amazon Special Projects team that takes the company’s Think Big leadership principle to the limits. If you’re interested in innovating at scale to address big challenges in the world, this is the team for you. As an Applied Scientist on our team, you will focus on building state-of-the-art ML models for healthcare. Our team rewards curiosity while maintaining a laser-focus in bringing products to market. Competitive candidates are responsive, flexible, and able to succeed within an open, collaborative, entrepreneurial, startup-like environment. At the forefront of both academic and applied research in this product area, you have the opportunity to work together with a diverse and talented team of scientists, engineers, and product managers and collaborate with other teams. This role offers a unique opportunity to work on projects that could fundamentally transform healthcare outcomes. Key job responsibilities In this role, you will: • Design and implement novel AI/ML solutions for complex healthcare challenges • Drive advancements in machine learning and data science • Balance theoretical knowledge with practical implementation • Work closely with customers and partners to understand their requirements • Navigate ambiguity and create clarity in early-stage product development • Collaborate with cross-functional teams while fostering innovation in a collaborative work environment to deliver impactful solutions • Establish best practices for ML experimentation, evaluation, development and deployment • Partner with leadership to define roadmap and strategic initiatives You’ll need a strong background in AI/ML, proven leadership skills, and the ability to translate complex concepts into actionable plans. You’ll also need to effectively translate research findings into practical solutions. A day in the life You will solve real-world problems by getting and analyzing large amounts of data, generate insights and opportunities, design simulations and experiments, and develop statistical and ML models. The team is driven by business needs, which requires collaboration with other Scientists, Engineers, and Product Managers across the Special Projects organization. You will prepare written and verbal presentations to share insights to audiences of varying levels of technical sophistication. About the team We represent Amazon's ambitious vision to solve the world's most pressing challenges. We are exploring new approaches to enhance research practices in the healthcare space, leveraging Amazon's scale and technological expertise. We operate with the agility of a startup while backed by Amazon's resources and operational excellence. We're looking for builders who are excited about working on ambitious, undefined problems and are comfortable with ambiguity.
Sr. Comm Systems Engineer, Wireless Systems
US, TX, Austin
Amazon Leo is an initiative to launch a constellation of Low Earth Orbit satellites that will provide low-latency, high-speed broadband connectivity to unserved and underserved communities around the world. As a Systems Engineer, this role is primarily responsible for the design, development and integration of communication payload and customer terminal systems. The Role: Be part of the team defining the overall communication system and architecture of Amazon Leo’s broadband wireless network. This is a unique opportunity to innovate and define groundbreaking wireless technology at global scale. The team develops and designs the communication system for project Leo and analyzes its overall system level performance such as for overall throughput, latency, system availability, packet loss etc. This role in particular will be responsible for leading the effort in designing and developing advanced technology and solutions for communication system. This role will also be responsible developing advanced physical layer + protocol stacks systems as proof of concept and reference implementation to improve the performance and reliability of the LEO network. In particular this role will be responsible for using concepts from digital signal processing, information theory, wireless communications to develop novel solutions for achieving ultra-high performance LEO network. This role will also be part of a team and develop simulation tools with particular emphasis on modeling the physical layer aspects such as advanced receiver modeling and abstraction, interference cancellation techniques, FEC abstraction models etc. This role will also play a critical role in the integration and verification of various HW and SW sub-systems as a part of system integration and link bring-up and verification. Export Control Requirement: Due to applicable export control laws and regulations, candidates must be a U.S. citizen or national, U.S. permanent resident (i.e., current Green Card holder), or lawfully admitted into the U.S. as a refugee or granted asylum.
Senior Applied Scientist, Real-Time Conversational AI , AGI
US, CA, Sunnyvale
We are looking for a Senior Applied Scientist to help drive the research and development of real-time multimodal conversational AI. You will contribute across two focus areas: advancing foundation models for speech and audio, and building the post-training systems (reward modeling, reinforcement learning) that shape natural, human-like conversational behavior. You will own a significant research area and contribute across the full model lifecycle — from pre-training and architecture design through post-training alignment and real-time deployment. You will work at the frontier of what’s possible in conversational AI, with the compute, data, and runway to pursue problems that few teams in the world have the resources to tackle. As a Senior Scientist, you will drive the technical execution of your research area, contribute to the team’s roadmap, and work closely with inference engineers to ensure your models are designed for real-time production deployment. Key job responsibilities What You’ll Do Foundation Model Scaling - Help build and train large-scale multimodal foundation models for real-time speech and audio generation, from architecture design through production-scale training - Advance the scaling and efficiency of conversational models, including the relationship between data, model size, and real-time performance - Design model architectures informed by hardware constraints and inference requirements, working with inference engineers to ensure models are servable from inception - Develop training methodologies for multimodal models that jointly process and generate speech, language, and audio in real-time streaming contexts - Contribute to the state of the art on efficient architectures and training methods for conversational AI at scale Post-Training & Reinforcement Learning - Design and build reward models and reward functions for speech systems — capturing naturalness, fluency, conversational quality, and real-time responsiveness - Develop and apply reinforcement learning methods to shape conversational behavior — teaching models natural timing, responsiveness, and fluid interaction - Build parts of the post-training pipeline from SFT through RL alignment, optimized for real-time multimodal outputs rather than text-only generation - Design evaluation frameworks that capture the quality dimensions unique to real-time conversation (latency sensitivity, audio quality, prosody, interaction naturalness) Real-Time Perception & Generation - Advance the team’s capabilities in real-time perception — the ability of the model to process incoming audio/speech while simultaneously generating responses - Develop techniques for natural interactive systems where the model handles concurrent input and output with human-like timing - Work at the intersection of model architecture and production constraints to ensure multimodal capabilities function within hard real-time latency budgets
Senior Applied Scientist, Fauna Robotics
US, WA, Bellevue
Robots are about to step out of the movies and into our homes. If you're excited about this robotics revolution, come join Amazon's Fauna Robotics. As an Applied Scientist in this org, you'll push the state-of-the-art techniques in Robotics. You'll drive technical excellence in areas such as perception, manipulation, sim2real transfer, reinforcement learning and multi-task learning, designing novel algorithms that bridge the gap between research and real-world deployment. In this role, you will integrate hands-on technical expertise with scientific leadership, ensuring your team delivers robust solutions for dynamic real-world environments. While staying updated with the latest advancements in robotics research, you will leverage your experience and expertise to guide the team towards the most promising direction. Collaborating with a talented group of software engineers and scientists, you will bring your ideas to fruition. Deploying robots in home environments requires you to anticipate challenges not encountered in structured settings like warehouses. Additionally, consumer-grade sensors and actuators necessitate working around their limitations, requiring out-of-the-box innovative ideas. As such, you are someone who truly enjoys thinking about problems using first principles at a holistic and systems level to address the aforementioned challenges. Key job responsibilities - Lead technical initiatives in areas such as robotics foundation models, reinforcement learning and manipulation - - Design experiments to identify the limitations of current state-of-the-art models and developing new models or techniques that can surpass these models - Design and implement novel deep learning architectures that push the boundaries of what robots can understand and accomplish - Mentor fellow scientists while maintaining strong individual technical contributions - Collaborate with engineering teams to optimize and scale models for real-world applications - Influence technical decisions and implementation strategies within your area of focus - Experienced in communicating complex technical work to a non-technical audience - The ability to work with minimal guidance, be proactive and to handle ambiguity and the challenge of quickly evolving goals A day in the life - Train ML models for deployment in simulation and real-world robots, identify and document their limitations post-deployment - Drive technical discussions within your team and with key stakeholders to develop innovative solutions to address identified limitations - Guide fellow scientists in solving complex technical challenges, from sim2real transfer to training RL policies - Mentor team members while maintaining significant hands-on contribution to technical solutions About the team Fauna Robotics, an Amazon company, is building capable, safe, and genuinely delightful robots for everyday life. Our goal is simple: make robots people actually want to live and interact with in everyday human spaces. We believe that future won’t arrive until building for robotics becomes far more accessible. Today, too much effort is spent reinventing the fundamentals. We’re changing that by developing tightly integrated hardware and software systems that make it faster, safer, and more intuitive to create real-world robotic products. Our work spans the full stack: mechanical design, control systems, dynamic modeling, and intelligent software. The focus is not just functionality, but experience. We’re building robots that feel responsive, expressive, and genuinely useful. At Fauna, you’ll work at the frontier of this space, helping define how robots move, manipulate, and interact with people in natural environments. It’s an opportunity to solve hard problems across hardware and software with a team focused on making robotics accessible and joyful to build. If you care about making robotics real for everyone and building systems that are as delightful as they are capable, we’re interested in hearing from you.
See more jobs
View from space of a connected network around planet Earth representing the Internet of Things.
Get more from Amazon Science
Subscribe to our newsletter

Amazon.com | Conditions of Use | Privacy | © 1996-2026 Amazon.com, Inc. or its affiliates

Social