Fix two false statements in lean_analysis_proofs
Maintainer thường phản hồi trong vòng 2 ngày
Chưa có ai nhận issue này.
Đánh giá
- Độ khó
- 3/5
- Thời gian dự kiến
- 1-2 ngày
- Mức phù hợp với người mới
- 56/100
- Loại issue
- Lỗi
- Độ rõ ràng
- Đặc tả rõ ràng
- Mức độ hoạt động
- Sôi nổi
- Công nghệ
- python
- Lĩnh vực
- testing-qa
Hướng nghiên cứu
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.
Do mô hình lập chỉ mục viết ra từ nội dung của issue.
Mô tả
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/.
- Ngôn ngữ chính
- SMT
- Star
- 477
- Fork
- 20
- Merge trung bình
- 3 ngày 6 giờ
- Pull request đã merge (30 ngày)
- 3
Chuẩn bị môi trường
- Không có Dockerfile hay tệp Docker Compose
- Có mẫu pull request
- Đọc hướng dẫn đóng góp
Bắt đầu từ đâu
- Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
- Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
- Fork repository và làm thay đổi trên một nhánh.
- Mở pull request có tham chiếu số hiệu của issue.
Issue khác của ByteDance-Seed/EdgeBench
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 73/100
ByteDance-Seed/EdgeBench#48 ·
Maintainer thường phản hồi trong vòng 2 ngày
-
FFmpeg: public result hides whether failure occurred before correctness checksCó thể đã có người làm @loopx-agent đã nhận 4 ngày trước. Đang mở
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100
ByteDance-Seed/EdgeBench#57 ·
Maintainer thường phản hồi trong vòng 2 ngày
-
integer_compression_codec: stored size anchors are impossible for the documented Varint starterĐang mở
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 54/100
ByteDance-Seed/EdgeBench#52 ·
Maintainer thường phản hồi trong vòng 2 ngày
-
wesnoth_tactical_ai: top-level Lua files never run (`if io then` raises on an undefined global)Đang mở
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 35/100
ByteDance-Seed/EdgeBench#51 ·
Maintainer thường phản hồi trong vòng 2 ngày
-
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 48/100
ByteDance-Seed/EdgeBench#50 ·
Maintainer thường phản hồi trong vòng 2 ngày
Tất cả issue của ByteDance-Seed/EdgeBench
Issue tương tự
-
area:tooling good first issue
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 68/100
interledger/publisher-tools#1007 ·
Maintainer thường phản hồi trong vòng 1 ngày
-
Criteria can pass when the deliverable is missingCó thể đã có người làm @clementtisseau đã nhận hôm nay. Đang mở
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 68/100
harveyai/harvey-labs#217 ·
Maintainer thường phản hồi trong vòng 2 ngày
-
area: ci good first issue
Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 85/100
interledger/web-monetization-extension#1555 ·
Maintainer thường phản hồi trong vòng 1 ngày
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
eyalgolan/statecraft-israel#3093 · 1 bình luận ·
Maintainer thường phản hồi trong vòng 1 ngày
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
Maintainer thường phản hồi trong vòng 1 ngày