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
Applied Scientist, FinAuto
IN, KA, Bengaluru
Interested to build the next generation Financial systems that can handle billions of dollars in transactions? Interested to build highly scalable next generation systems that could utilize Amazon Cloud? Massive data volume + complex business rules in a highly distributed and service oriented architecture, a world class information collection and delivery challenge. Our challenge is to deliver the software systems which accurately capture, process, and report on the huge volume of financial transactions that are generated each day as millions of customers make purchases, as thousands of Vendors and Partners are paid, as inventory moves in and out of warehouses, as commissions are calculated, and as taxes are collected in hundreds of jurisdictions worldwide. Key job responsibilities • Understand the business and discover actionable insights from large volumes of data through application of machine learning, statistics or causal inference. • Analyse and extract relevant information from large amounts of Amazon’s historical transactions data to help automate and optimize key processes • Research, develop and implement novel machine learning and statistical approaches for anomaly, theft, fraud, abusive and wasteful transactions detection. • Use machine learning and analytical techniques to create scalable solutions for business problems. • Identify new areas where machine learning can be applied for solving business problems. • Partner with developers and business teams to put your models in production. • Mentor other scientists and engineers in the use of ML techniques. A day in the life • Understand the business and discover actionable insights from large volumes of data through application of machine learning, statistics or causal inference. • Analyse and extract relevant information from large amounts of Amazon’s historical transactions data to help automate and optimize key processes • Research, develop and implement novel machine learning and statistical approaches for anomaly, theft, fraud, abusive and wasteful transactions detection. • Use machine learning and analytical techniques to create scalable solutions for business problems. • Identify new areas where machine learning can be applied for solving business problems. • Partner with developers and business teams to put your models in production. • Mentor other scientists and engineers in the use of ML techniques. About the team The FinAuto TFAW(theft, fraud, abuse, waste) team is part of FGBS Org and focuses on building applications utilizing machine learning models to identify and prevent theft, fraud, abusive and wasteful(TFAW) financial transactions across Amazon. Our mission is to prevent every single TFAW transaction. As a Machine Learning Scientist in the team, you will be driving the TFAW Sciences roadmap, conduct research to develop state-of-the-art solutions through a combination of data mining, statistical and machine learning techniques, and coordinate with Engineering team to put these models into production. You will need to collaborate effectively with internal stakeholders, cross-functional teams to solve problems, create operational efficiencies, and deliver successfully against high organizational standards.
Applied Scientist III, AGI Responsible AI (RAI)
US, CA, Sunnyvale
Amazon's Artificial General Intelligence (AGI) organization is seeking an Applied Scientist III to advance the science of Responsible AI evaluation for large language models and generative AI. In this role, you will lead the design and development of rigorous evaluation methods, benchmarks, and metrics that measure the safety, fairness, robustness, and trustworthiness of frontier models. You will work with large-scale datasets, modern deep learning frameworks, and world-class scientists and engineers to turn research into evaluation systems that shape model launch decisions at Amazon scale. Key job responsibilities - Lead the design and implementation of evaluation frameworks, benchmarks, and metrics for responsible AI, including safety, fairness, robustness, and harmful content. - Build scalable automated evaluation pipelines for large language models, including model-based and human-in-the-loop evaluation. - Partner with pretraining, post-training, and product teams to translate evaluation results into model improvements and launch decisions. - Conduct rigorous experimentation and statistical analysis, and publish research at top venues. - Mentor junior scientists and help raise the scientific bar of the team. - Champion responsible AI practices across the model development lifecycle. About the team The AGI Responsible AI (RAI) team builds the science and systems that make Amazon's large language models safe, fair, and trustworthy. We work on problems spanning safety evaluation, content moderation, watermarking, bias mitigation, and alignment. Our team values scientific rigor, customer obsession, and rapid iteration, and we collaborate closely with pretraining, post-training, and product teams across AGI.
Principal Audio Scientist, Fauna
US, NY, New York
Fauna Robotics is building capable, safe, and delightful robots for everyday life, and voice is one of the most natural ways people will interact with them. Cloud speech and language models are good and getting better, but they can only work with the audio they receive, and a robot is a hard place to listen. Its microphones sit beside motors, fans, and moving joints. It speaks through its own loudspeaker while people talk over it. It moves, turns, and shares a room with several people at once. We are hiring a Principal Audio Scientist to be Fauna's technical authority on how our robots hear. You will design, prototype, and ship the hardest algorithms in the robot's audio system. You will set the audio architecture that other engineers build on, shape hardware decisions across robot generations, mentor the engineers and scientists working on audio, and be the person teams come to when the robot can't hear. Key job responsibilities - Set the long-range science roadmap and technical architecture for the robot's audio system, and serve as Fauna's primary technical authority on robot hearing - Design and implement suppression of the robot's own noise from motors, fans, and moving joints - Design and implement echo cancellation for the robot's own voice, so people can interrupt it naturally - Develop multi-microphone processing that holds up as the robot and the people around it move, including locating who is speaking so the robot can turn toward them - Make on-robot listening decisions robust to internal and external noise sources: wake word, voice activity, and whether speech is directed at the robot - Drive microphone and speaker placement, enclosure acoustics, and vibration isolation decisions with mechanical, electrical, and industrial design, backed by your own measurements - Design the robot-specific data collection and evaluation methods to validate the performance of our audio design - Present audio science and its tradeoffs to senior leadership and partner teams - Mentor scientists and engineers, raising the scientific bar for audio across the organization through design reviews, code reviews, and hiring
Robotics/AI Motor Control Scientist, Fauna
US, NY, New York
We are seeking a Robotics/AI Motor Control Scientist to develop cutting-edge machine learning algorithms for motor control systems in robots. In this role, you will focus on creating and optimizing intelligent motor control strategies to enable robots to perform complex, whole-body tasks. Your contributions will be essential in advancing robotics by enabling fluid, reliable, and safe interactions between robots and their environments. Key job responsibilities - Develop controllers that leverage reinforcement learning, imitation learning, or other advanced AI techniques to achieve natural, robust, and adaptive motor behaviors - Collaborate with multi-disciplinary teams to integrate motor control systems with robotic hardware, ensuring alignment with real-world constraints such as actuator dynamics and energy efficiency - Use simulation and real-world testing to refine and validate control algorithms - Stay updated on advancements in robotics, AI, and control systems to apply advanced techniques to robotic motion challenges - Lead technical projects from conception through production deployment - Mentor junior scientists and engineers - Bridge research initiatives with practical engineering implementation 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. 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.
(Senior) AI Engineer - Reinforcement Learning Manipulation, RIVR
CH, Zurich
RIVR, an Amazon company, is building Physical AI by deploying autonomous robots for real-world doorstep delivery. Operating daily in diverse urban environments, RIVR's robots continuously learn from and navigate the millions of scenarios encountered during deliveries. By owning the full stack from software to hardware, RIVR is purpose-built for safety, reliability, and the customer from day one. Reinforcement learning is transforming our robotic intelligence, enabling autonomous behavior without human guidance. We are seeking a Senior AI Engineer with deep expertise in reinforcement learning and deep learning, including supervised and self-supervised learning with a focus on dexterous manipulation. Your role will involve leveraging both simulated and real-world data to address practical challenges in dynamic grasping, contact-rich manipulation, and object interaction. If you are passionate about advancing AI and developing innovative solutions, join us in shaping the future of intelligent robotics. Key job responsibilities Develop cutting-edge reinforcement learning algorithms to enable robust, contact-rich dexterous manipulation, translating vision, depth, tactile, and proprioceptive sensor input into precise end-effector and joint-level motor commands. Design, test, and refine algorithms to solve complex real-world manipulation challenges, such as handling diverse package form factors, dynamic hand-offs, and operating door handles or latches. Collaborate with the foundation model team to innovate methods that leverage both simulated and real-world data.
Applied Scientist, TSI Science
US, WA, Seattle
Do you want to join an innovative team of scientists who use machine learning and statistical techniques to help Amazon provide the best customer experience by preventing eCommerce fraud? Are you excited by the prospect of analyzing and modeling terabytes of data and creating state-of-the-art algorithms to solve real world problems? Do you like to own end-to-end business problems/metrics and directly impact the profitability of the company? Do you enjoy collaborating in a diverse team environment? If yes, then you may be a great fit to join the Amazon Selling Partner Trust & Store Integrity Science Team. We are looking for a talented scientist who is passionate to build advanced machine learning systems that help manage the safety of millions of transactions every day and scale up our operation with automation. Key job responsibilities Innovate with the latest GenAI/LLM/VLM technology to build highly automated solutions for efficient fraud detection, risk evaluation and automated operations Design, develop and deploy end-to-end advance machine learning solutions with vision anf GenAi technologies in the Amazon production environment to create impactful business value Learn, explore and experiment with the latest machine learning advancements to create the best customer experience A day in the life You will be working within a dynamic, diverse, and supportive group of scientists who share your passion for innovation and excellence. You'll be working closely with business partners and engineering teams to create end-to-end scalable machine learning solutions that address real-world problems. You will build scalable, efficient, and automated processes for large-scale data analyses, model development, model validation, and model implementation. You will also be providing clear and compelling reports for your solutions and contributing to the ongoing innovation and knowledge-sharing that are central to the team's success.
Applied Scientist, AGI/AI Security
US, NY, New York
We are seeking an Applied Scientist to contribute to research and development of novel security validation and monitoring techniques for AI systems at scale. You will own and contribute to four critical work-streams: 1. Real-Time Agent Monitoring Design and implement scientific approaches for continuous behavioral analysis of AI agents in production—detecting anomalous actions, prompt injection exploitation, and policy violations in real time. 2. Protection & Automated Remediation Invent and deliver novel protection technologies and automated remediation techniques building on research in security, cryptography, privacy, automated reasoning, and others domains, to enable safe and secure agentic AI models and AI applications. 3. AI Application and Capabilities Validation Invent and deliver scalable methodologies for security testing of AI applications and AI capabilities (e.g. MCP, skills), including adversarial robustness evaluation, safety guardrail bypass detection, tool-use authorization boundaries, and trust boundary verification. 4. AI Asset Discovery & Inventory Research and build scalable techniques to automatically discover, identify, and catalog all AI-enabled applications, services, and capabilities across the company—maintaining a comprehensive, continuously updated database of AI assets. Key job responsibilities Invent • Identify and frame new research challenges in AI security where problems are ill-defined and require novel scientific paradigms at the product level. • Contribute to the team's scientific agenda for agent monitoring, protection, remediation, validation research, and AI asset discovery. • Publish research results at peer-reviewed internal and external venues (e.g., USENIX Security, ACM CCS, IEEE S&P, NeurIPS, ICML security workshops, ICSE, PETS) when appropriate. • Articulate key scientific challenges of current and future AI security threats and deliver novel research to address them. • Design, implementation, and successful delivery of scientifically complex security solutions into production—both brand new systems and evolutions of existing ones. • Write significant portions of critical-path code for detection models, validation engines, protection technologies, and asset discovery / classification systems. • Assess and select appropriate technologies (e.g., data protection, private inference, graph-based anomaly detection, NLP-based service classification, code/traffic analysis for AI fingerprinting) for production systems. • Use best practices in scientific methodology and software engineering across the team; provide insightful peer reviews of code, design, and architecture artifacts. • Deliver solutions that are inventive, maintainable, scalable, and extensible. Influence • Autonomously drive discussions with security engineers, software engineers, product managers, and scientist peers across multiple teams. • Build consensus on larger cross-team security initiatives and factor complex efforts into independent workstreams. • Identify and resolve endemic problems, including areas where current security tooling limits innovation of partner teams. • Contribute to the broader internal and external scientific communities as a subject matter expert in AI security. About the team Diverse Experiences Amazon Security 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 Security? At Amazon, security is central to maintaining customer trust and delivering delightful customer experiences. Our organization is responsible for creating and maintaining a high bar for security across all of Amazon’s products and services. We offer talented security professionals the chance to accelerate their careers with opportunities to build experience in a wide variety of areas including cloud, devices, retail, entertainment, healthcare, operations, and physical stores. Inclusive Team Culture In Amazon Security, it’s in our nature to learn and be curious. Ongoing DEI events and learning experiences inspire us to continue learning and to embrace our uniqueness. Addressing the toughest security challenges requires that we seek out and celebrate a diversity of ideas, perspectives, and voices. Training & 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, training, 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 flexible work hours and arrangements are part of our culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve.
Applied Scientist II, Last Mile Science
IN, KA, Bangalore
Amazon’s Last Mile Team is looking for a passionate individual with strong optimization and analytical skills to join its Last Mile Science team in the endeavor of designing and improving the most complex planning of delivery network in the world. Last Mile builds global solutions that enable Amazon to attract an elastic supply of drivers, companies, and assets needed to deliver Amazon's and other shippers' volumes at the lowest cost and with the best customer delivery experience. Last Mile Science team owns the core decision models in the space of jurisdiction planning, delivery channel and modes network design, capacity planning for on the road and at delivery stations, routing inputs estimation and optimization. Our research has direct impact on customer experience, driver and station associate experience, Delivery Service Partner (DSP)’s success and the sustainable growth of Amazon. Optimizing the last mile delivery requires deep understanding of transportation, supply chain management, pricing strategies and forecasting. Only through innovative and strategic thinking, we will make the right capital investments in technology, assets and infrastructures that allows for long-term success. Our team members have an opportunity to be on the forefront of supply chain thought leadership by working on some of the most difficult problems in the industry with some of the best product managers, scientists, and software engineers in the industry. Key job responsibilities Candidates will be responsible for developing solutions to better manage and optimize delivery capacity in the last mile network. The successful candidate should have solid research experience in one or more technical areas of Operations Research or Machine Learning. These positions will focus on identifying and analyzing opportunities to improve existing algorithms and also on optimizing the system policies across the management of external delivery service providers and internal planning strategies. They require superior logical thinkers who are able to quickly approach large ambiguous problems, turn high-level business requirements into mathematical models, identify the right solution approach, and contribute to the software development for production systems. To support their proposals, candidates should be able to independently mine and analyze data, and be able to use any necessary programming and statistical analysis software to do so. Successful candidates must thrive in fast-paced environments, which encourage collaborative and creative problem solving, be able to measure and estimate risks, constructively critique peer research, and align research focuses with the Amazon's strategic needs. As a senior scientist, you will also help coach/mentor junior scientists in the team.
Senior Applied Scientist, Fauna
US, NY, New York
We are seeking an Applied Scientist to lead the development of evaluation frameworks and data collection protocols for robotic capabilities. In this role, you will focus on designing how we measure, stress-test, and improve robot behavior across a wide range of real-world tasks. Your work will play a critical role in shaping how policies are validated and how high-quality datasets are generated to accelerate system performance. You will operate at the intersection of robotics, machine learning, and human-in-the-loop systems, building the infrastructure and methodologies that connect teleoperation, evaluation, and learning. This includes developing evaluation policies, defining task structures, and contributing to operator-facing interfaces that enable scalable and reliable data collection. The ideal candidate is highly experimental, systems-oriented, and comfortable working across software, robotics, and data pipelines, with a strong focus on turning ambiguous capability goals into measurable and actionable evaluation systems. Key job responsibilities - Design and implement evaluation frameworks to measure robot capabilities across structured tasks, edge cases, and real-world scenarios - Develop task definitions, success criteria, and benchmarking methodologies that enable consistent and reproducible evaluation of policies - Create and refine data collection protocols that generate high-quality, task-relevant datasets aligned with model development needs - Build and iterate on teleoperation workflows and operator interfaces to support efficient, reliable, and scalable data collection - Analyze evaluation results and collected data to identify performance gaps, failure modes, and opportunities for targeted data collection - Collaborate with engineering teams to integrate evaluation tooling, logging systems, and data pipelines into the broader robotics stack - Stay current with advances in robotics, evaluation methodologies, and human-in-the-loop learning to continuously improve internal approaches - Lead technical projects from conception through production deployment - Mentor junior scientists and engineers
Satellite GNC Engineer, Amazon Leo
US, WA, Redmond
Amazon Leo is building a constellation of thousands of low Earth orbit satellites to deliver fast, reliable internet beyond the reach of existing networks. As a Guidance, Navigation & Control engineer, you will design the algorithms, simulations, and onboard autonomy that keep every satellite precisely pointed and stable so the payload can serve customers below, and keep the fleet flying safely. This is satellite GNC with demanding pointing and performance requirements, and you will see your work go from concept to orbit on a constellation that is launching and growing today. Amazon Leo will delight customers with reliable connectivity regardless of where they are. In this role, you will: - Take your GNC algorithms from concept all the way to orbit, and stay close to them through integration, test, and on-orbit operations - Solve hard precise-pointing, payload-cueing, and fleet-autonomy problems against demanding performance requirements - Work across the full lifecycle — design, simulation, test, and flight operations — rather than a narrow slice - Join a small team of some of the top GNC engineers in the industry, building a product people will love to use This position is part of the Satellite Attitude Determination and Control team, where we own the full lifecycle of our work — from algorithm design and flight software, through lab integration, to flying our own satellites on orbit. You will design and analyze the control system and algorithms, support development of our flight hardware and software, help integrate the satellite in our labs, and operate the GNC system in flight as a constellation of satellites flows through the production line into orbit. **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. Key job responsibilities - Design and analyze algorithms for state estimation, attitude determination and control, precise pointing, and payload cueing against demanding performance requirements. - Write the production C++ flight code that runs these algorithms on the satellite. Our GNC engineers own their algorithms all the way into flight software, working alongside software development engineers rather than handing prototypes off to be reimplemented by another team. - Design concepts of operation that balance pointing and payload cueing, momentum management, power, thermal, and communications across all phases of the mission, including off-nominal and contingency scenarios. - Develop momentum management strategies using reaction wheels and magnetic torquers, and help size and lay out the GNC sensor and actuator suite — star trackers, magnetometers, sun sensors, IMUs, and GPS receivers — and the algorithms that consume them. - Develop onboard autonomy, including Fault Detection, Isolation, and Recovery, so the fleet operates safely at scale with minimal intervention. - Develop and validate models and simulations of the satellite and constellation across a range of fidelity levels, including 6-DOF time-domain simulation and Monte Carlo analysis, and run hardware-in-the-loop testing to verify closed-loop performance. - Support component-level environmental testing, functional and performance checkout, and subsystem and satellite integration in our labs. - Analyze fleet telemetry in bulk and build the metrics, dashboards, and tooling that let us monitor and continuously improve pointing performance and payload operations time as the constellation grows. - Operate the GNC system on orbit — reviewing fleet data, supporting maneuvers, and resolving anomalies when on-orbit behavior diverges from the ground model. - Contribute to architecture, design, and code reviews, and document your algorithms, analyses, and results clearly. A day in the life This role spans a diverse set of problems across the spacecraft and network system. You will derive and prototype estimation and control algorithms, turn them into production flight code, and prove them out through 6-DOF and Monte Carlo simulation and hardware-in-the-loop testing in the lab. You will support satellite integration, and when something on orbit does not behave the way the ground model predicted, you will dig into fleet telemetry to find out why and drive the fix. You will own problems end to end and have the focus to go deep on each one. Because GNC sits at the center of safe flight, you will work across the whole program. The payload, power, thermal, and operations teams all depend on GNC, so you will balance their needs against your pointing and momentum budgets. To get your algorithms running reliably on the spacecraft, you will partner closely with avionics, flight software, and our embedded software development engineers. You will help the mechanical teams shape the next generation of satellite hardware, from reaction wheels to star trackers. And as satellites move from design through manufacturing into orbit, you will work alongside systems engineering and Assembly, Integration & Test. The problems are genuinely hard — demanding pointing and performance requirements, a large constellation to keep flying safely, and the chance to invent advanced capabilities that have not been built before. The work is staffed with some of the strongest engineers in the industry, and the constant collaboration across teams makes it a place to keep learning and growing. About the team Our team brings deep experience across many satellite systems and other flight vehicles, with real bench strength in both our mission and the core GNC disciplines. We design, prototype, test, iterate, and learn together, and because GNC is central to safe flight, we tend to drive Concepts of Operation and many of the system-level analyses on the program. We also have a lot of freedom. We trust our engineers to pursue the problems they face in whatever way they find best, to choose their own tools and approaches, and to own the results. If you want the autonomy to solve hard problems your way, and a team of strong engineers to do it with, you will feel at home here.
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