Fix two false statements in lean_analysis_proofs
I maintainer di solito rispondono entro 2 giorni
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 3/5
- Tempo stimato
- 1-2 giorni
- Idoneità per principianti
- 56/100
- Tipo di issue
- Bug
- Chiarezza
- Specificata chiaramente
- Stato di attività
- Attiva
- Stack tecnologico
- python
- Ambito
- testing-qa
Direzione di ricerca
Read the Lean theorem statements for PiecewiseConstantOn.div and MajorizesOn.anti_symm, then compare them with the linked upstream fixes. Also inspect the project’s Lean version configuration and update it from 4.28.0 to 4.35.0; done means both statements match the fixes and the project uses the requested Lean version. The payload does not name files or tests, so locate the declarations and version setting in the repository.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
The task snapshot contains two false theorem statements already corrected upstream:
- PiecewiseConstantOn.div: the second hypothesis constrains f instead of g. Upstream fix.
- MajorizesOn.anti_symm: missing parentheses give the universal quantifier the wrong scope. Upstream fix.
Additionally, the Lean version should be updated to 4.35.0, as 4.28.0 is vulnerable to various exploits that can allow trivial discharging of proofs - https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/.
- Lingua principale
- Python
- Stelle
- 474
- Fork
- 20
- Merge medio
- 1g 7h
- PR unite (30g)
- 2
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Nessun modello di pull request
- Leggi la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di ByteDance-Seed/EdgeBench
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 62/100
ByteDance-Seed/EdgeBench#46 ·
I maintainer di solito rispondono entro 2 giorni
-
warehouse_forklift_routing: `TIME_LIMIT = 60` kills inputs within the stated 30 s per test caseAperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 35/100
ByteDance-Seed/EdgeBench#47 ·
I maintainer di solito rispondono entro 2 giorni
-
smt_solver: correct models on six hard files crash the validator and score the whole submission 0Aperta
Difficoltà 4/5 3-5 giorni Idoneità per principianti 22/100
ByteDance-Seed/EdgeBench#42 ·
I maintainer di solito rispondono entro 2 giorni
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 18/100
ByteDance-Seed/EdgeBench#40 ·
I maintainer di solito rispondono entro 2 giorni
-
Difficoltà 3/5 1-2 giorni Idoneità per principianti 35/100
ByteDance-Seed/EdgeBench#39 ·
I maintainer di solito rispondono entro 2 giorni
Tutte le issue di ByteDance-Seed/EdgeBench
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 64/100
FinanceFlash/unvibecode#577 · 1 commento ·
I maintainer di solito rispondono entro 1 giorno
-
area/test type/bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 76/100
Clodmony/starship-coop#70 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 77/100
punitarani/fli#270 ·
-
🐛 Bug 🔔 Pending processing
Difficoltà 2/5 1-3 ore Idoneità per principianti 67/100
jumpserver/jumpserver#17980 ·
I maintainer di solito rispondono entro 1 giorno
-
community enhancement good first issue
Difficoltà 2/5 1-3 ore Idoneità per principianti 86/100
I maintainer di solito rispondono entro 1 giorno