Repository navigation
Conversation
There was a problem hiding this comment.
Pull request overview
Vendored import of an external bounded-arithmetic formalization (Cook–Nguyen-style two-sorted logic: IOPEN, IΔ0, V0, plus string addition commutativity/associativity). Adds project metadata, an entry module, and ~14 supporting Lean files covering language definitions (Peano, Zambella), syntax/semantics infrastructure, complexity classes, displayed-variable plumbing, and the carry-induction proofs for str_add_comm/str_add_assoc.
Holistic assessment:
- Fit: good_fit — Cook–Nguyen bounded arithmetic is a recognized research program; this is theory-building, not one-off problem-solving.
- Level: graduate
- Branch: mathematical logic / proof complexity
- Mode: theory_building
- Obscure problem: false
- Code quality: 3 — substantial scaffolding, but with rough edges (commented-out blocks, TODOs, redundant
PartialOrder numinstance declared twice inV0.lean, twoCanonicallyOrderedAdd numinstances, verbose carry-comm vialeanstral-generated proofs as the authors themselves note). - Significance: Formalizes finite axiomatization of V0 and derives associativity/commutativity of two-sorted string addition from a strengthened carry invariant — a genuine fragment of the Cook–Nguyen program rather than a single lemma.
- Verdict: approve
Changes:
- New project entry in
LeanPool/projects.ymland rootLeanPool.leanimport additions. - New module tree under
LeanPool/FormalizationOfBoundedArithmetic/implementing two-sorted language, complexity hierarchy, IOPEN/IΔ0/V0 models, and string-addition theorems. - Top-level project card
LeanPool/FormalizationOfBoundedArithmetic.lean.
Reviewed changes
Copilot reviewed 22 out of 22 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
| LeanPool/projects.yml | Adds the project entry with declarations, tags, MSC. |
| LeanPool.lean | Adds auto-generated imports for new modules. |
| LeanPool/FormalizationOfBoundedArithmetic.lean | Top-level project card aggregating imports. |
| LeanPool/FormalizationOfBoundedArithmetic/V0.lean | V0 model class, xmin/xind, comp-to-induction. |
| LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean | Commutativity of string addition via carry symmetry. |
| LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean | Associativity via strengthened carry invariant + propositional induction. |
| LeanPool/FormalizationOfBoundedArithmetic/IOPEN.lean | IOPEN model and basic ring-like theorems by open induction. |
| LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean | IΔ0 model, predecessor, cancellation, order instances. |
| LeanPool/FormalizationOfBoundedArithmetic/BasicSingleSorted.lean | BASIC axioms and pairing notation. |
| LeanPool/FormalizationOfBoundedArithmetic/LanguagePeano.lean | Peano first-order language definition. |
| LeanPool/FormalizationOfBoundedArithmetic/LanguageZambella.lean | Two-sorted Zambella language and ZambellaModel class. |
| LeanPool/FormalizationOfBoundedArithmetic/Syntax.lean | iSup'/iAlls'/iExs' over enumerated types and relabel lemmas. |
| LeanPool/FormalizationOfBoundedArithmetic/Semantics.lean | Realize lemmas and peel_iAlls'/peel_iExs' conv tactics. |
| LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean | IsOpen/IsDelta0/IsSigma0B with relabel/display lemmas. |
| LeanPool/FormalizationOfBoundedArithmetic/AxiomSchemes.lean | mkInductionSentence and mkComprehensionSentence builders. |
| LeanPool/FormalizationOfBoundedArithmetic/Order.lean | Bounded quantifier formulas iBdEx'/iBdAll'/iBdAllLt'. |
| LeanPool/FormalizationOfBoundedArithmetic/Algebra.lean | Mathlib algebraic instances on IOPEN/IΔ0 models. |
| LeanPool/FormalizationOfBoundedArithmetic/DisplayedVariables.lean | Vars1..Vars4, display/rotate/flip relabels. |
| LeanPool/FormalizationOfBoundedArithmetic/IsEnum.lean | IsEnum class + deriving handler. |
| LeanPool/FormalizationOfBoundedArithmetic/Register.lean | Registers the delta0_simps simp attribute. |
| LeanPool/FormalizationOfBoundedArithmetic/SimpRules.lean | Seeds delta0_simps with Sum/Function lemmas. |
| LeanPool/FormalizationOfBoundedArithmetic/MathlibSimps.lean | Pulls existing Mathlib model-theory simp lemmas into delta0_simps. |
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | 🟡 borderline |
| Level | graduate |
| Branch | mathematical logic / proof complexity |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is bounded-arithmetic infrastructure and string-addition laws for a strengthened V0-style interface, not a formal derivation of these laws from the finite V0 axiomatization.
Findings (2)
- statement-mismatch —
LeanPool/FormalizationOfBoundedArithmetic/V0.lean:29
V0Modelis introduced near comments about finite axiomatizability of V0, but the class includes strong extra fields such as propositional induction, open/delta-zero induction, decidable order, cancellation, and algebraic laws. The project card mostly says this, but the Lean interface itself should make the distinction hard to miss, e.g. by separating a raw V0 axiom class from the strengthened downstream interface or by consistently naming the class as strengthened. - overlapping-instance —
LeanPool/FormalizationOfBoundedArithmetic/V0.lean:143
This file creates multiple global instances for the same algebra/order classes under[V0Model num str], notablyPartialOrderandCanonicallyOrderedAdd; similar empty/derived instances appear inAlgebra.lean. Keep a single canonical instance per class or avoid registering the auxiliary structures as global instances, since otherwise downstream typeclass search can pick non-obvious paths through the strengthened fields.
Tokens: 80,346 in / 2,586 out · Tier: standard · Cost: $0.4793
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
|
/profile |
Proof profile (new / modified Lean files)
This is the parallel build wall clock and is the compile-time answer for this PR. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 9,551 maxHeartbeats units across 21 files (6,276 added LOC). Sum of Count-heartbeats wall-clock total: 62.02 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.FormalizationOfBoundedArithmetic.V0StrSuccAssoc |
5.20 s |
LeanPool.FormalizationOfBoundedArithmetic.IOPEN |
4.40 s |
LeanPool.FormalizationOfBoundedArithmetic.V0 |
4.40 s |
LeanPool.FormalizationOfBoundedArithmetic.MathlibSimps |
4.20 s |
LeanPool.FormalizationOfBoundedArithmetic.IDelta0 |
4.20 s |
LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm |
4.00 s |
LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables |
3.90 s |
LeanPool.FormalizationOfBoundedArithmetic.V0StrAddAssoc |
3.80 s |
LeanPool.FormalizationOfBoundedArithmetic.Syntax |
3.70 s |
LeanPool.FormalizationOfBoundedArithmetic.Semantics |
3.20 s |
LeanPool.FormalizationOfBoundedArithmetic.BasicSingleSorted |
3.00 s |
LeanPool.FormalizationOfBoundedArithmetic.Complexity |
2.80 s |
Per-file `lean --profile` output
LeanPool/FormalizationOfBoundedArithmetic.lean
import took 2.03s
cumulative profiling times:
elaboration 0.116ms
import 2.03s
initialization 26.5ms
interpretation 218ms
linting 0.237ms
parsing 0.028ms
real 2.87
user 1.68
sys 1.20
LeanPool/FormalizationOfBoundedArithmetic/Algebra.lean
import took 2.03s
cumulative profiling times:
attribute application 1.32ms
compilation (IR) 0.215ms
compilation (LCNF base) 3.85ms
compilation (LCNF impure) 0.93ms
compilation (LCNF mono) 3.42ms
congr simp thm 0.165ms
elaboration 134ms
fix level params 0.351ms
import 2.03s
initialization 26.6ms
instantiate metavars 0.473ms
interpretation 297ms
let-to-have transformation 0.258ms
linting 4.25ms
parsing 2.87ms
process pre-definitions 6.92ms
share common exprs 0.682ms
simp 2.19ms
tactic execution 35.7ms
type checking 18.5ms
typeclass inference 173ms
real 3.22
user 2.18
sys 1.17
LeanPool/FormalizationOfBoundedArithmetic/AxiomSchemes.lean
import took 1.22s
elaboration took 108ms
cumulative profiling times:
attribute application 0.357ms
blocked (unaccounted) 111ms
compilation (IR) 2.4ms
compilation (LCNF base) 55.6ms
compilation (LCNF impure) 12ms
compilation (LCNF mono) 21ms
elaboration 265ms
fix level params 0.231ms
import 1.22s
initialization 26.6ms
instantiate metavars 0.221ms
interpretation 217ms
let-to-have transformation 1.53ms
linting 10.7ms
parsing 5.27ms
process pre-definitions 6.74ms
share common exprs 0.845ms
type checking 3.52ms
typeclass inference 30.9ms
real 2.39
user 1.69
sys 0.80
LeanPool/FormalizationOfBoundedArithmetic/BasicSingleSorted.lean
import took 1.23s
cumulative profiling times:
attribute application 0.684ms
blocked (unaccounted) 56.3ms
compilation (IR) 0.669ms
compilation (LCNF base) 30.7ms
compilation (LCNF impure) 3.8ms
compilation (LCNF mono) 8.1ms
elaboration 87.1ms
fix level params 0.176ms
import 1.23s
initialization 27ms
instantiate metavars 0.127ms
interpretation 196ms
let-to-have transformation 0.107ms
linting 5.05ms
parsing 4.37ms
process pre-definitions 6.58ms
share common exprs 0.738ms
tactic execution 7.11ms
type checking 19.3ms
typeclass inference 64.8ms
real 2.17
user 1.51
sys 0.80
LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean
import took 1.21s
cumulative profiling times:
attribute application 18.2ms
blocked (unaccounted) 220ms
compilation (IR) 0.313ms
compilation (LCNF base) 10.3ms
compilation (LCNF impure) 2.08ms
compilation (LCNF mono) 3.68ms
congr simp thm 4.08ms
elaboration 237ms
fix level params 4.85ms
import 1.21s
initialization 26.8ms
instantiate metavars 8.07ms
interpretation 631ms
let-to-have transformation 0.693ms
linting 37.9ms
parsing 26.2ms
process pre-definitions 16.7ms
share common exprs 11.5ms
simp 51.5ms
tactic execution 238ms
type checking 127ms
typeclass inference 115ms
real 2.47
user 2.51
sys 0.85
LeanPool/FormalizationOfBoundedArithmetic/DisplayedVariables.lean
import took 1.12s
cumulative profiling times:
attribute application 20.8ms
blocked (unaccounted) 5.31ms
compilation (IR) 3.57ms
compilation (LCNF base) 30.6ms
compilation (LCNF impure) 18.9ms
compilation (LCNF mono) 30.4ms
congr simp thm 1.82ms
elaboration 235ms
fix level params 1.05ms
import 1.12s
initialization 26.9ms
instantiate metavars 4.83ms
interpretation 418ms
let-to-have transformation 0.394ms
linting 20.1ms
parsing 27.6ms
process pre-definitions 31.3ms
share common exprs 3.93ms
simp 93.9ms
tactic execution 43.8ms
type checking 73.7ms
typeclass inference 69.9ms
real 2.37
user 2.19
sys 0.78
LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean
import took 2.08s
tactic execution of Lean.Parser.Tactic.specialize took 1.11s
cumulative profiling times:
attribute application 1.02ms
blocked (unaccounted) 0.579ms
compilation (IR) 0.258ms
compilation (LCNF base) 3.78ms
compilation (LCNF impure) 1.42ms
compilation (LCNF mono) 3.11ms
congr simp thm 4.76ms
elaboration 109ms
fix level params 4.08ms
import 2.08s
initialization 27.1ms
instantiate metavars 7.6ms
interpretation 584ms
let-to-have transformation 0.225ms
linting 23.2ms
parsing 21.6ms
process pre-definitions 22.1ms
share common exprs 11.3ms
simp 378ms
tactic execution 1.73s
type checking 97.5ms
typeclass inference 324ms
real 4.68
user 4.86
sys 1.24
LeanPool/FormalizationOfBoundedArithmetic/IOPEN.lean
import took 2.05s
simp took 309ms
simp took 310ms
simp took 315ms
simp took 322ms
simp took 322ms
simp took 314ms
simp took 311ms
simp took 312ms
simp took 309ms
simp took 308ms
simp took 706ms
simp took 533ms
cumulative profiling times:
attribute application 0.252ms
blocked (unaccounted) 0.582ms
compilation (IR) 0.158ms
compilation (LCNF base) 1.31ms
compilation (LCNF impure) 1.57ms
compilation (LCNF mono) 1.46ms
congr simp thm 98.5ms
elaboration 94.3ms
fix level params 7.54ms
import 2.05s
initialization 26.6ms
instantiate metavars 7.08ms
interpretation 550ms
let-to-have transformation 0.226ms
linting 18.5ms
parsing 17.2ms
process pre-definitions 20.3ms
share common exprs 21.5ms
simp 5.12s
tactic execution 573ms
type checking 160ms
typeclass inference 315ms
real 4.81
user 8.51
sys 1.19
LeanPool/FormalizationOfBoundedArithmetic/IsEnum.lean
import took 1.01s
elaboration took 137ms
cumulative profiling times:
attribute application 0.135ms
blocked (unaccounted) 0.465ms
compilation (IR) 1.52ms
compilation (LCNF base) 68.4ms
compilation (LCNF impure) 10.1ms
compilation (LCNF mono) 25.4ms
congr simp thm 0.108ms
dsimp 0.662ms
elaboration 159ms
fix level params 0.18ms
import 1.01s
initialization 26.5ms
instantiate metavars 0.177ms
interpretation 192ms
let-to-have transformation 2.87ms
linting 14.6ms
parsing 6.17ms
process pre-definitions 5.9ms
share common exprs 1.5ms
simp 0.466ms
tactic execution 112ms
type checking 11ms
typeclass inference 118ms
real 2.24
user 1.66
sys 0.70
LeanPool/FormalizationOfBoundedArithmetic/LanguagePeano.lean
import took 1.21s
cumulative profiling times:
attribute application 7.6ms
blocked (unaccounted) 73.5ms
compilation (IR) 1.4ms
compilation (LCNF base) 43.4ms
compilation (LCNF impure) 7.3ms
compilation (LCNF mono) 14.3ms
congr simp thm 0.095ms
elaboration 75.9ms
fix level params 0.352ms
import 1.21s
initialization 26.8ms
instantiate metavars 0.475ms
interpretation 297ms
let-to-have transformation 0.164ms
linting 7.16ms
parsing 5.71ms
process pre-definitions 11.5ms
share common exprs 1.39ms
simp 0.944ms
tactic execution 0.552ms
type checking 12.7ms
typeclass inference 57.2ms
real 2.22
user 1.61
sys 0.79
LeanPool/FormalizationOfBoundedArithmetic/LanguageZambella.lean
import took 1.22s
cumulative profiling times:
attribute application 10.4ms
blocked (unaccounted) 65.4ms
compilation (IR) 2.06ms
compilation (LCNF base) 46.1ms
compilation (LCNF impure) 9.84ms
compilation (LCNF mono) 19.9ms
congr simp thm 1.79ms
elaboration 223ms
fix level params 0.874ms
import 1.22s
initialization 26.7ms
instantiate metavars 1.02ms
interpretation 370ms
let-to-have transformation 0.273ms
linting 13.9ms
parsing 16.1ms
process pre-definitions 16.1ms
share common exprs 2.25ms
simp 15.6ms
tactic execution 20.2ms
type checking 45.4ms
typeclass inference 75.2ms
real 2.37
user 1.94
sys 0.84
LeanPool/FormalizationOfBoundedArithmetic/MathlibSimps.lean
import took 1.23s
interpretation of _aux_LeanPool_FormalizationOfBoundedArithmetic_MathlibSimps___elabRules_commandMkDelta0FromModelTheory_1._boxed took 865ms
cumulative profiling times:
attribute application 142ms
blocked (unaccounted) 64.3ms
compilation (IR) 0.769ms
compilation (LCNF base) 38.3ms
compilation (LCNF impure) 4.72ms
compilation (LCNF mono) 12.1ms
elaboration 22.2ms
fix level params 0.0245ms
import 1.23s
initialization 26.9ms
instantiate metavars 0.00637ms
interpretation 1.01s
let-to-have transformation 0.837ms
linting 2.56ms
parsing 0.775ms
process pre-definitions 1.04ms
share common exprs 0.181ms
type checking 49.6ms
typeclass inference 11.4ms
real 3.05
user 2.30
sys 0.84
LeanPool/FormalizationOfBoundedArithmetic/Order.lean
import took 1.23s
cumulative profiling times:
attribute application 0.0842ms
compilation (IR) 0.871ms
compilation (LCNF base) 12.6ms
compilation (LCNF impure) 4.47ms
compilation (LCNF mono) 9.92ms
congr simp thm 2.64ms
elaboration 71.9ms
fix level params 2.08ms
import 1.23s
initialization 26.7ms
instantiate metavars 4.62ms
interpretation 292ms
let-to-have transformation 0.659ms
linting 7.57ms
parsing 8.4ms
process pre-definitions 8.49ms
share common exprs 5.93ms
simp 109ms
tactic execution 144ms
type checking 38.5ms
typeclass inference 34.4ms
real 2.20
user 1.76
sys 0.81
LeanPool/FormalizationOfBoundedArithmetic/Register.lean
import took 796ms
cumulative profiling times:
attribute application 0.273ms
blocked (unaccounted) 7.18ms
compilation (IR) 0.29ms
compilation (LCNF base) 3.3ms
compilation (LCNF impure) 1.68ms
compilation (LCNF mono) 3.12ms
elaboration 5.54ms
fix level params 0.024ms
import 796ms
initialization 26.6ms
instantiate metavars 0.0192ms
interpretation 5.08ms
let-to-have transformation 0.0205ms
linting 0.386ms
parsing 0.182ms
process pre-definitions 0.854ms
share common exprs 0.113ms
tactic execution 1.54ms
type checking 0.352ms
typeclass inference 2.05ms
real 1.37
user 0.77
sys 0.62
LeanPool/FormalizationOfBoundedArithmetic/Semantics.lean
import took 1.23s
cumulative profiling times:
attribute application 18ms
blocked (unaccounted) 193ms
compilation (IR) 1.65ms
compilation (LCNF base) 119ms
compilation (LCNF impure) 10.2ms
compilation (LCNF mono) 22.7ms
congr simp thm 7.44ms
dsimp 35.2ms
elaboration 318ms
fix level params 4.16ms
import 1.23s
initialization 26.9ms
instantiate metavars 4.18ms
interpretation 742ms
let-to-have transformation 0.52ms
linting 32.2ms
parsing 30.6ms
process pre-definitions 19.9ms
share common exprs 13.6ms
simp 306ms
tactic execution 267ms
type checking 106ms
typeclass inference 308ms
real 2.85
user 3.38
sys 0.83
LeanPool/FormalizationOfBoundedArithmetic/SimpRules.lean
import took 1.23s
cumulative profiling times:
attribute application 0.87ms
elaboration 0.423ms
import 1.23s
initialization 26.9ms
interpretation 123ms
linting 0.249ms
parsing 0.0643ms
real 1.93
user 1.14
sys 0.80
LeanPool/FormalizationOfBoundedArithmetic/Syntax.lean
import took 1.13s
cumulative profiling times:
attribute application 27.1ms
blocked (unaccounted) 37ms
compilation (IR) 0.601ms
compilation (LCNF base) 5.87ms
compilation (LCNF impure) 2.7ms
compilation (LCNF mono) 6.36ms
congr simp thm 14.6ms
dsimp 79.6ms
elaboration 155ms
fix level params 2.15ms
import 1.13s
initialization 27.3ms
instantiate metavars 2.02ms
interpretation 330ms
let-to-have transformation 0.902ms
linting 15.9ms
parsing 14.8ms
process pre-definitions 7.17ms
share common exprs 4.94ms
simp 213ms
tactic execution 239ms
type checking 84.8ms
typeclass inference 152ms
real 2.27
user 2.28
sys 0.80
LeanPool/FormalizationOfBoundedArithmetic/V0.lean
import took 2.03s
elaboration took 129ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 248ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 280ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 719ms
cumulative profiling times:
attribute application 2.17ms
blocked (unaccounted) 98.4ms
compilation (IR) 0.341ms
compilation (LCNF base) 6.23ms
compilation (LCNF impure) 2.03ms
compilation (LCNF mono) 14.1ms
congr simp thm 0.563ms
elaboration 373ms
fix level params 3.32ms
import 2.03s
initialization 26.6ms
instantiate metavars 12.8ms
interpretation 2s
let-to-have transformation 0.338ms
linting 41.8ms
parsing 39.2ms
process pre-definitions 25.2ms
share common exprs 9.49ms
simp 17.4ms
tactic execution 727ms
type checking 197ms
typeclass inference 591ms
real 4.64
user 5.50
sys 1.26
LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean
import took 2.08s
cumulative profiling times:
attribute application 0.0665ms
congr simp thm 7.59ms
elaboration 51.3ms
fix level params 1.1ms
import 2.08s
initialization 27.1ms
instantiate metavars 15.3ms
interpretation 489ms
let-to-have transformation 0.0629ms
linting 24.9ms
parsing 9.18ms
process pre-definitions 17.6ms
share common exprs 26.5ms
simp 690ms
tactic execution 408ms
type checking 44.7ms
typeclass inference 44.4ms
real 3.75
user 3.32
sys 1.27
LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean
import took 2.07s
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 604ms
cumulative profiling times:
attribute application 0.0355ms
elaboration 11.3ms
fix level params 0.592ms
import 2.07s
initialization 26.9ms
instantiate metavars 5.2ms
interpretation 890ms
let-to-have transformation 0.0288ms
linting 3.46ms
parsing 3.15ms
process pre-definitions 3.88ms
share common exprs 1.73ms
tactic execution 210ms
type checking 8.01ms
typeclass inference 38.9ms
real 3.75
user 2.71
sys 1.19
LeanPool/FormalizationOfBoundedArithmetic/V0StrSuccAssoc.lean
import took 2.09s
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 332ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 327ms
cumulative profiling times:
attribute application 0.423ms
blocked (unaccounted) 472ms
congr simp thm 1.34ms
elaboration 175ms
fix level params 8.12ms
import 2.09s
initialization 26.8ms
instantiate metavars 22.2ms
interpretation 1.71s
let-to-have transformation 0.446ms
linting 68.1ms
parsing 77.7ms
process pre-definitions 39.6ms
share common exprs 20ms
simp 50.1ms
tactic execution 1.5s
type checking 100ms
typeclass inference 1.35s
real 4.28
user 6.61
sys 1.25
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
|
Deterministic partial-port audit flags this PR as incomplete against the registered upstream source. Compared with Because the project card advertises V0 string results, omitting the upstream This is the failure mode automated in #110. |
|
/review |
|
Follow-up on the partial-port audit: the specific omitted headline file from that audit is now present. Commit |
|
/profile |
|
Follow-up on the partial-port/source-anchor review items: the branch is now updated to current Changes in this update:
Local checks passed:
The original missing- |
|
/review |
|
LLM review skipped: Lean Action CI conclusion was |
|
/review |
|
Follow-up on the remaining LLM request-changes item: commit Local checks passed after the update:
This should address the semantic framing issue without changing the imported proofs. |
|
/review |
|
Follow-up to the latest LLM The PR now calls the project Local verification passed:
I'll rerun the LLM reviewer after CI is green on this head. |
|
/review |
|
Second follow-up to the remaining Because the project-card generator only renders declaration names, I added explicit alias theorem names and changed the metadata to list those aliases instead of the raw theorem names:
The detailed Local verification passed:
|
|
/review |
|
Final framing tweak pushed in |
|
/review |
|
Latest reviewer result on |
|
/review |
|
Follow-up audit for the partial-port flag: the reported missing Against current upstream |
Imported from https://github.com/ruplet/formalization-of-bounded-arithmetic.
Slug:
formalization-of-bounded-arithmeticToolchain target:
leanprover/lean4:v4.30.0-rc2Branch:
import/formalization-of-bounded-arithmetic-retry-20260518-144229(retry run20260518-144229)Agent:
codexusinggpt-5.5at effortxhigh.Commits on this branch:
Opened manually after
scripts/import-formalization.shfinished the agent run but exited before PR creation due to the running wrapper script seeingmainchange under it. The branch was rebased onto currentorigin/mainand checked for content-only diff before push.