leanprover-community/batteries

Develop the `List.sum`, `List.prod` and related APIs

Open

#1,465 opened on Oct 16, 2025

View on GitHub
 (0 comments) (0 reactions) (0 assignees)Lean (154 forks)auto 404
enhancementhelp wanted

Repository metrics

Stars
 (406 stars)
PR merge metrics
 (PR metrics pending)

Description

Mathlib's BigOperators library is well-developed, sophisticated and works extremely well. There is however a need for a less sophisticated intermediate library built directly on Std's basic classes for associativity, commutativity, identities. Just downstreaming Mathlib's API is not possible since many features don't fit in Batteries' focus on programming and formal verification.

We need a plan for this. This plan should balance low-level and high-level features, enhancing Std's basic API in a manner compatible with Mathlib's API. This plan should strengthen both Std and Mathlib, while staying within the scope of Batteries.

Contributor guide

Research direction
Explore the existing Std List.sum and List.prod implementations and Mathlib's BigOperators to design an intermediate API that fits Batteries' focus on programming and formal verification.
Tech stack
None
Domain
backend api design
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-2 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Fresh
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Needs investigation
Prerequisites
LeanStdMathlib
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
20