sahibzada-allahyar/YC-Killer

[Physics Copilot] E3-08 — Canonical Lean examples (30)

Open

#39 opened on Nov 2, 2025

View on GitHub
 (0 comments) (0 reactions) (0 assignees)TypeScript (126 forks)auto 404
area:leanhelp wantedsize:Stype:task

Repository metrics

Stars
 (2,780 stars)
PR merge metrics
 (PR metrics pending)

Description

Summary Add 30 canonical math examples with expected outcomes.

Repo Context

Acceptance Criteria

  • 20 pass; 10 fail with clear messages

Tasks

  • Examples dir
  • Golden traces

Test Plan

  • Example runner.

LOC & Simplicity Guardrails

Definition of Done

  • CI green, unit/integration tests added.
  • Docs updated.
  • Demo snippet or example under physics_copilot/examples/.

Contributor guide

Research direction
Create a directory for examples, write 20 passing and 10 failing Lean examples with clear error messages, and set up a test runner to verify.
Tech stack
None
Domain
documentation
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.
Half day
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.
Mostly clear
Prerequisites
LeanGit
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
70