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 Inference Engineer, AGI
US, CA, Sunnyvale
We are looking for a Senior Inference Engineer to own inference for real-time multimodal conversational AI. This is a full-stack inference role: you will work across the entire path a model takes from research to production — shaping model architecture so it is servable, building the real-time runtime that serves it within hard latency budgets, and building the offline systems that train and reinforce it. You will operate at the boundary of Science and Inference, taking frontier-scale speech and audio models and making them run within real-time latency budgets on production hardware. You will co-design architectures with scientists to make them inference-friendly from inception, own the low-latency streaming serving path, and build the training and reinforcement-learning infrastructure that closes the loop. You will have the compute, data, and runway to solve problems that few teams in the world are positioned to tackle. As a Senior Engineer, you will own a significant area of the inference stack end to end, drive its technical execution, contribute to the team's roadmap, and work closely with scientists and hardware partners to ensure our models run fast enough to feel human in real time — and at a cost that makes them viable at scale. You may go deep in one of the areas below while contributing across the others. Key job responsibilities Model Architecture & Inference Co-Design • Partner with research scientists to make model architectures servable from inception — surfacing the latency, memory, and cost implications of architecture choices before they are locked in • Implement and optimize the inference path for large-scale multimodal models — attention and KV-cache mechanisms, multimodal/autoregressive decoding, and the compute primitives on the critical path Apply efficiency techniques across the stack — quantization (per-tensor/per-channel/per- group, INT8/FP8/BF16), speculative decoding, operator fusion, and paged KV-cache — and quantify their quality/latency trade-offs • Develop and tune high-performance kernels for critical operations where off-the-shelf implementations leave performance on the table, integrating them into production serving with minimal overhead • Profile end-to-end performance with tools such as Nsight Compute/Systems and roofline analysis to identify and eliminate bottlenecks in large-scale inference workloads Real-Time & Interactive Runtime • Own the real-time serving path for streaming multimodal conversational AI, meeting sub- second, streaming latency budgets under concurrent session load • Build and tune continuous batching, scheduling, and preemption to balance throughput against per-request latency SLAs for interactive workloads • Customize production serving frameworks (e.g., vLLM, PyTorch) for real-time streaming generative models that fall outside standard LLM serving patterns — sustained low-latency output under concurrent session load • Implement multi-GPU inference (tensor parallelism, collective communication) for latency- critical paths, and drive cost toward parity with existing production baselines • Establish latency, throughput, and cost benchmarking, and publish the operational metrics that gate deployment Offline Systems: Training, RL & Evaluation Infrastructure • Build and scale the offline inference systems behind post-training — high-throughput rollout generation and reward-model serving for reinforcement learning (RL/RLHF/RLAIF) • Ensure train/serve consistency — that the inference path used in RL and evaluation faithfully matches production online behavior (e.g., parity across sampling and logit processing) • Work with the evaluation team to enable offline inference that captures the quality dimensions unique to real-time conversation — latency sensitivity, audio quality, and interaction naturalness
Applied Scientist, Last Mile Science
US, TX, Austin
Are You Ready to Redefine How the World Receives Its Packages? What if your algorithms defined the most efficient path for millions of deliveries — every single day? At Amazon, we're building the science that makes that possible, and we're looking for exceptional scientists to help lead the way. The Last Mile Routing & Planning organization develops the software, algorithms, and tools that power the "magic" of home delivery. Our planning and routing intelligence systems drive billions of daily decisions — enabling safe, efficient, and frustration-free routes for drivers across the globe. What You'll Do In this role, you'll sit at the intersection of state-of-the-art research and real-world impact. You will: - Design and build algorithms that solve large-scale, complex logistics problems - Synthesize data from diverse sources to identify high-value business opportunities - Provide research direction and data-driven insights to guide strategic decisions - Translate complex technical approaches into clear communication for scientists, engineers, and business stakeholders - Partner closely with scientists and engineers in a collaborative, high-impact environment What You'll Work On We have an exciting and growing portfolio of research areas, including: - Routing for same-day and grocery deliveries - Planning for electric and autonomous vehicles - District-level and stop-level planning - Forecasting solutions for diverse delivery programs All of this is powered by the latest methods in Operations Research (OR), Machine Learning (ML), and Generative AI — at a truly global scale. Successful candidates will lead one or more of these problem spaces. What We're Looking For - Deep expertise in Operations Research and/or Machine Learning methods - Proven experience applying these methods to large-scale, real-world business problems - Ability to translate models into production-ready code in Python or Java - Strong communication skills — you can explain complex technical concepts to diverse audiences - A bias for action and an iterative mindset when tackling ambitious research challenges Why Amazon We're passionate about your growth. Whether you want to explore emerging technologies, take on broader scope, or accelerate your career trajectory, we'll invest in helping you get there. Our business is scaling fast — and so are the opportunities for the people who build it. If you're driven by the challenge of optimizing one of the world's most complex logistics systems and excited to see your work impact millions of customers daily, we'd love to hear from you. Key job responsibilities - Invent and design novel solutions for scientifically complex problem areas, and identify opportunities for invention within existing and new business initiatives - Deliver large-scale, high-impact solutions to complex problems in support of medium-to-large business goals - Shape the design of scientifically complex software systems, personally contributing significant portions of the critical scientific novelty - Apply mathematical optimization, machine learning, and Generative AI techniques to develop solution methodologies for in-house decision support tools and software - Research, prototype, simulate, and experiment with models — and actively participate in their production-level deployment in Python or Java - Engage with the broader scientific community by publishing research articles and participating in leading research conferences
Flight Dynamics Engineer, Amazon Leo Flight Dynamics
US, WA, Redmond
We are searching for a talented candidate with experience in orbital mechanics, orbit determination, launch vehicle trajectories, and launch vehicle mission planning. In this position, a successful candidate would serve as a Research Scientist in support of Amazon Leo’s constellation with particular focus on Launch Vehicle support. Strong analysis skills are required to develop engineering studies of complex large-scale dynamical systems. This position requires demonstrated expertise in computational analysis automation and tool development. 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 Working with the Leo GNC team, you will: • Perform spacecraft maneuver or navigation analysis in support of multi-disciplinary trades within the Amazon Leo team. • Contribute to prototype software development of flight algorithms. • Test and assess navigation software for integration into flight systems. • Assess and trouble-shoot the performance of Leo on-board GNSS hardware and software systems. • Work closely with GNC engineers to manage on-orbit performance and develop flight dynamics operations processes. • Manage engineering trades as needed for various launch vehicle mission designs. • Support Leo’s Launch Vehicle Mission Management team with technical expertise in Launch Vehicle trajectory requirements specification • Evaluate Launch Vehicle performance and compliance with mission requirements • Develop tools to support Mission Management planning for over 80 launches! • Work collaboratively with launch vehicle system technical teams About the team The Flight Dynamics team is responsible for the guidance, navigation, control and safety of the spaceflight of the Amazon Leo constellation. This team provides solutions to spaceflight challenges in constellation design, orbit selection, launch vehicle insertion requirements, navigation, trajectory design, space situational awareness, and space traffic coordination.
Principal Applied Scientist, Real-Time Conversational AI , AGI
US, WA, Seattle
We are looking for a Principal Applied Scientist to drive the research and development of real-time multimodal conversational AI. You will operate 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 be the expert in your area while contributing 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 Principal Scientist, you will set the technical direction for your research area, influence the broader roadmap, and work closely with inference engineers to ensure your models are designed for real-time production deployment from inception. Key job responsibilities Foundation Model Scaling - 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 modes, 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 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 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 Real-Time Perception & Generation - Advance the team's capabilities in real-time perception - Work at the intersection of model architecture and production constraints to ensure multimodal capabilities function within hard real-time latency budgets
Applied Scientist II, Amazon Robotics
DE, Berlin
The Amazon Robotics team is seeking an experienced Applied Scientist to join our team. In this role you will apply the latest trends in research to solve real-world problems in robotics and AI. You will collaborate with a team of scientists and engineers building these applications. We holistically design, build, and deliver end-to-end robotic systems. Our team is also responsible for core infrastructure and tools that serve as the backbone of our robotic applications, enabling roboticists, machine learning scientists, software engineers, and hardware engineers to collaborate and deploy systems in the field. Key job responsibilities • Research, design, develop, and evaluate complex perception, motion planning, and decision making algorithms integrating across multiple disciplines and leveraging machine learning. • Create experiments and prototype implementations of new learning algorithms and prediction techniques. • Work closely with software engineering team members to drive scalable, real-time implementations. • Collaborate with machine learning and robotic controls experts to implement and deploy algorithms, such as machine learning models. • Collaborate closely with hardware engineering team members on developing systems from prototyping to production level. • Represent Amazon in academia community through publications and scientific presentations. • Work with stakeholders across hardware, science, and operations teams to iterate on systems design and implementation. About the team Watch this video to learn more about Vulcan Pick team in Amazon Robotics: https://www.amazon.science/publications/vulcan-pick-a-robotic-system-for-picking-targeted-objects-from-fabric-pods
Data Scientist, Alexa AI
IN, KA, Bengaluru
Amazon is looking for a passionate, talented, and inventive Data Scientist with machine learning background to help build industry-leading Speech and Language technology. Our mission is to provide a delightful experience to Amazon’s customers by pushing the envelope in Automatic Speech Recognition (ASR), Natural Language Understanding (NLU), Machine Learning (ML). Key job responsibilities Key job responsibilities Amazon is looking for a passionate, talented, and inventive Data Scientist with machine learning background to help build industry-leading Speech and Language technology. Our mission is to provide a delightful experience to Amazon’s customers by pushing the envelope in Automatic Speech Recognition (ASR), Natural Language Understanding (NLU), Machine Learning (ML) and Computer Vision (CV). As part of our AI team in Amazon AWS, you will work alongside internationally recognized experts to develop data experiments, novel algorithms and data techniques to advance the state-of-the-art in human language technology. Your work will directly impact millions of our customers in the form of products and services that make use of speech and language technology. You will gain hands on experience with Amazon’s heterogeneous speech, text, and structured data sources, and large-scale computing resources to accelerate advances in spoken language understanding.
PhD Econ Intern, Store Economics and Science
US, WA, Seattle
We are looking for detail-oriented, organized, and responsible individuals who are eager to learn how to apply their causal inference / structural econometrics skillsets to solve real world problems. The intern will work in the area of Store Economics and Science (SEAS) and develop models to SEAS. Our PhD Economist Internship Program offers hands-on experience in applied economics, supported by mentorship, structured feedback, and professional development. Interns work on real business and research problems, building skills that prepare them for full-time economist roles at Amazon and beyond. You will learn how to build data sets and perform applied econometric analysis collaborating with economists, scientists, and product managers. These skills will translate well into writing applied chapters in your dissertation and provide you with work experience that may help you with placement. About the team The Stores Economics and Science Team (SEAS) is a Stores-wide interdisciplinary team at Amazon with a "peak jumping" mission focused on disruptive innovation. The team applies science, economics, and engineering expertise to tackle the business's most critical problems, working to move from local to global optima across Amazon Stores operations. SEAS builds partnerships with organizations throughout Amazon Stores to pursue this mission, exploring frontier science while learning from the experience and perspective of others. Their approach involves testing solutions first at a small scale, then aligning more broadly to build scalable solutions that can be implemented across the organization. The team works backwards from customers using their unique scientific expertise to add value, takes on long-run and high-risk projects that business teams typically wouldn't pursue, helps teams with kickstart problems by building practical prototypes, raises the scientific bar at Amazon, and builds and shares software that makes Amazon more productive.
Applied Scientist , Prime Video Personalization and Discovery
US, WA, Seattle
Prime Video is a first-stop entertainment destination offering customers a vast collection of premium programming in one app available across thousands of devices. Prime members can customize their viewing experience and find their favorite movies, series, documentaries, and live sports – including Amazon MGM Studios-produced series and movies; licensed fan favorites; and programming from Prime Video add-on subscriptions such as Apple TV+, Max, Crunchyroll and MGM+. All customers, regardless of whether they have a Prime membership or not, can rent or buy titles via the Prime Video Store, and can enjoy even more content for free with ads. Are you interested in shaping the future of entertainment? Prime Video's technology teams are creating best-in-class digital video experience. As a Prime Video technologist, you’ll have end-to-end ownership of the product, user experience, design, and technology required to deliver state-of-the-art experiences for our customers. You’ll get to work on projects that are fast-paced, challenging, and varied. You’ll also be able to experiment with new possibilities, take risks, and collaborate with remarkable people. We’ll look for you to bring your diverse perspectives, ideas, and skill-sets to make Prime Video even better for our customers. With global opportunities for talented technologists, you can decide where a career Prime Video Tech takes you! We are looking for a self-motivated, passionate and resourceful Applied Scientist to bring diverse perspectives, ideas, and skill-sets to make Prime Video even better for our customers. You will spend your time as a hands-on machine learning practitioner and a research leader. You will play a key role on the team, building and guiding machine learning models from the ground up. At the end of the day, you will have the reward of seeing your contributions benefit millions of Amazon.com customers worldwide. Key job responsibilities Develop AI solutions for various Prime Video Personalization systems using Deep learning, GenAI, Reinforcement Learning, and optimization methods; Work closely with engineers and product managers to design, implement and launch AI solutions end-to-end; Design and conduct offline and online (A/B) experiments to evaluate proposed solutions based on in-depth data analyses; Effectively communicate technical and non-technical ideas with teammates and stakeholders; Stay up-to-date with advancements and the latest modeling techniques in the field; Publish your research findings in top conferences and journals. About the team Prime Video Personalization and Discovery team owns science solution to power personalized experience on various devices, from sourcing, relevance, ranking, to name a few. We work closely with the engineering and product teams to launch our solutions in production.
Applied Scientist II, International Machine Learning
IN, KA, Bengaluru
Do you want to join an innovative team of scientists who use machine learning and statistical techniques to create state-of-the-art solutions for providing better value to Amazon’s customers? Do you want to build and deploy advanced ML systems that help optimize millions of transactions every day? Are you excited by the prospect of analyzing and modeling terabytes of data 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 like to innovate and simplify? If yes, then you may be a great fit to join the Machine Learning team for India Consumer Businesses. Machine Learning, Big Data and related quantitative sciences have been strategic to Amazon from the early years. Amazon has been a pioneer in areas such as recommendation engines, ecommerce fraud detection and large-scale optimization of fulfillment center operations. As Amazon has rapidly grown and diversified, the opportunity for applying machine learning has exploded. We have a very broad collection of practical problems where machine learning systems can dramatically improve the customer experience, reduce cost, and drive speed and automation. These include product bundle recommendations for millions of products, safeguarding financial transactions across by building the risk models, improving catalog quality via extracting product attribute values from structured/unstructured data for millions of products, enhancing address quality by powering customer suggestions We are developing state-of-the-art machine learning solutions to accelerate the Amazon India growth story. Amazon India is an exciting place to be at for a machine learning practitioner. We have the eagerness of a fresh startup to absorb machine learning solutions, and the scale of a mature firm to help support their development at the same time. As part of the India Machine Learning team, you will get to work alongside brilliant minds motivated to solve real-world machine learning problems that make a difference to millions of our customers. We encourage thought leadership and blue ocean thinking in ML. Key job responsibilities Use machine learning and analytical techniques to create scalable solutions for business problems Analyze and extract relevant information from large amounts of Amazon’s historical business data to help automate and optimize key processes Design, develop, evaluate and deploy, innovative and highly scalable ML models Work closely with software engineering teams to drive real-time model implementations Work closely with business partners to identify problems and propose machine learning solutions Establish scalable, efficient, automated processes for large scale data analyses, model development, model validation and model maintenance Work proactively with engineering teams and product managers to evangelize new algorithms and drive the implementation of large-scale complex ML models in production Leading projects and mentoring other scientists, engineers in the use of ML techniques About the team International Machine Learning Team is responsible for building novel ML solutions that attack India first (and other Emerging Markets across MENA and LatAm) problems and impact the bottom-line and top-line of India business. Learn more about our team from https://www.amazon.science/working-at-amazon/how-rajeev-rastogis-machine-learning-team-in-india-develops-innovations-for-customers-worldwide
Applied Scientist II, Amazon Recommerce India
IN, KA, Bengaluru
Every product a customer returns is a moment where Amazon either recovers value or writes it off — and India's ReCommerce business is on a multi-million-dollar mission to recover more of it, more intelligently, at scale. Machine learning is the core lever: predicting whether a returned unit is sellable without a human touching it, detecting damage and fraud inside sealed packaging from images, routing each unit to its highest-value disposition, and pricing recovered inventory dynamically. India's returns network is large, fast-growing, and structurally different from other geographies — a rich, high-impact environment for an Applied Scientist to build models that move real financial and customer-experience metrics. We are hiring an Applied Scientist to build and adapt the ML that powers India ReCommerce. You will work at the intersection of two mandates: building India-first models for problems unique to our market, and adapting proven Worldwide models to India's data, catalog, and operational reality — recalibrating them where distribution, language, and process differ. You will own problems end-to-end, from framing and data through modeling, evaluation, and production deployment, partnering closely with engineering, product, and operations. Key job responsibilities Build ML models for automated returns grading — predicting the salability of returned units from structured and unstructured signals so units can be evaluated with zero or minimal human touch, improving speed, accuracy, and recovery value. Develop computer-vision models for defect detection, condition assessment, and anomaly/fraud identification (including inside sealed packaging), and for establishing chain-of-custody and damage attribution across the returns journey. Build disposition-prediction and routing models that direct each unit to its highest-value recovery path (resale, repair, liquidation, donation, recycle) as early as possible in the network. Develop pricing and recovery-optimization models for liquidation and resale, moving from flat rates toward dynamic, grade- and condition-aware pricing. Adapt Worldwide ML models to India — retraining, recalibrating, and re-evaluating for India's return distribution, catalog, languages, and operational constraints, and closing the gaps that prevent a direct lift-and-shift. Own the full model lifecycle — problem framing, data pipelines, feature engineering, training, offline/online evaluation, monitoring, and retraining — with rigorous attention to calibration, drift, and business-metric impact. Partner cross-functionally with engineering (to productionize), product (to frame problems and measure impact), and operations (to ground models in how the network actually runs), and use modern GenAI/LLM tooling to accelerate research and delivery. A day in the life You start by reviewing the performance of a grading model in production — checking calibration and drift against last week's returns, and confirming the recovery-value lift is holding. Mid-morning, you dig into a computer-vision problem: improving detection of a damage type that's driving write-offs, using images captured across the returns journey. In the afternoon you work with a Worldwide science team to bring one of their models to India — scoping what retraining and recalibration India's data requires — then pair with an engineer to move your latest model toward production behind a clean evaluation gate. You close by framing a new problem with a product partner: quantifying the opportunity, defining the label and success metric, and sketching the modeling approach. About the team India ReCommerce owns the systems and science that turn returned and unsellable inventory into recovered value and a better customer experience. You will join a team building an increasingly automated, ML-driven returns network — leveraging Worldwide platforms where they fit and building India-first capabilities where they don't. It is a high-ownership environment with a direct line from your models to measurable business and customer outcomes.
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