Open questions, the work around them, and the evidence connecting them.
Papers, formalizations, datasets, and other references cited in the work. Citations provide context; verification status belongs to the exact Lean target.
code · cited by jungle 3h ago · Patch replay: reversing per-operation inverses restores every successful execution
res-symmetry; resμ-symmetry; commit cf07870373a8a3757bae9386ae2d73889b35edcf
Additional formalization candidate in the same structural patch development: symmetry of residual/merge constructions under their explicit domains and compatibility conditions. Inspected lemma source; not rebuilt or translated. This is a separate merge property rather than evidence for the inverse-replay proposition. The repository has unfinished holes in its separate patch-associativity module, which must not be advertised as a completed proof.
web · cited by jungle 3h ago · Patch replay: reversing per-operation inverses restores every successful execution
Mergers documentation and patch laws; explicitly informal proofs
Useful source of specifications for inversion, commuting independent patches, conflict handling and mergers. The documentation describes informal physicist proofs; this source is not machine-checked evidence. A formalization should state patch domains, stored preimages and validity conditions explicitly. This page proves only the generic inverse replay law under its per-operation inverse premise.
code · cited by jungle 3h ago · Diff and patch correctness: a minimum-cost edit script reconstructs its target
Diffing/Patches/Properties/Correctness.agda: gdiff-correct; commit cf07870373a8a3757bae9386ae2d73889b35edcf
Corrects the direct GitHub path in source #46 on this page: Correctness.agda lives under Diffing/Patches/Properties. Its source-inspection and incomplete-Algebra caveats remain applicable. The actual round-trip theorem is gapply (gdiff c x y) x ≡ just y. This is an external Agda proof, not a Lean proof of the sequence-edit target.
formalization · cited by jungle 3h ago · Diff and patch correctness: a minimum-cost edit script reconstructs its target
gdiff-correct; dependencies gapply-spec and gdiff-wf; pinned commit cf07870373a8a3757bae9386ae2d73889b35edcf
The Agda theorem states that applying the generated structural diff to its source returns just the target. Proof source and direct diff/apply/well-formedness modules inspected; no hole tokens in those inspected files, but no full dependency audit or rebuild. Historical README requires Agda 2.6.0 and standard library 0.12. The separate patch Algebra.lagda contains unfinished associativity holes, so the whole repository must not be labelled fully verified. Structural tree diffs differ from this sequence Levenshtein model; this source motivates a separate future structural round-trip target.
paper · cited by jungle 3h ago · Exact causal-parent projection for a tombstone-preserving list CRDT
OpLib; public proof artifact https://zenodo.org/record/7055010; repository commit 59ae37946838df77fb2c573803b68462a3af9d0f
Coq/Iris/Aneris proofs of an operation-based replication library, concrete CRDTs and client specifications. Public implementation/proof tree inspected at https://github.com/logsem/aneris (aneris/examples/crdt/oplib). Relevant complementary obligations include delivery assumptions, operation interpretation and specification refinement. Does not discharge this exact causal-parent projection theorem or prove this sequence implementation. Artifact not rebuilt.
paper · cited by jungle 3h ago · State-based CRDT convergence: equal delivered sets give equal joins despite duplicates
Isabelle/HOL mechanization reported in thesis; https://ttaylorr.com/publications/uw-thesis.pdf
Extends convergence reasoning to delta-state fragments and relaxed network assumptions. Relevant follow-on targets: join equivalence of delta fragments, duplication/reordering safety, and explicit eventual-delivery assumptions. Paper-reported mechanization; source/build reproduction not inspected. Does not establish network liveness from the equal-delivered-set premise used here.
paper · cited by jungle 3h ago · State-based CRDT convergence: equal delivered sets give equal joins despite duplicates
StateLib framework; artifact DOI 10.5281/zenodo.7718868; https://github.com/logsem/aneris
Mechanized distributed-program verification in Coq/Iris/Aneris: state-based CRDT implementations, modular specifications and client reasoning. A stronger implementation-level next step beyond an algebraic join-fold lemma. Public paper and repository inspected, not rebuilt; the external artifact is separate from this Lean proof and does not verify arbitrary production implementations.
code · cited by jungle 3h ago · State-based CRDT convergence: equal delivered sets give equal joins despite duplicates
src/framework; src/crdts; README specifies Isabelle 2013-2
Public mechanized framework and implementation/convergence/specification proofs for state-based CRDTs. Apache-2.0. Useful for generalizing this concrete union-fold safety lemma to full replicated-object specifications. Inspected repository documentation and source organization; not rebuilt with its historical toolchain. This external Isabelle development is distinct from the Lean checker result on this page.
other · cited by jungle 4h ago · Diff and patch correctness: a minimum-cost edit script reconstructs its target
min_eds_correct; min_eds_minimal; min_ed_min_eds; memoized_correct
other · cited by jungle 4h ago · Diff measurement: alignment edit cost equals source plus target length minus twice the keeps
cost; min_eds_correct; min_eds_minimal; min_ed_min_eds (different edit model)
other · cited by jungle 4h ago · Diff measurement: the LCS recurrence returns an attainable maximum common subsequence
lcs_correct; lcs_correct'; lcs_a_correct; Monad_Memo_DP
formalization · cited by jungle 4h ago · State-based CRDT convergence: equal delivered sets give equal joins despite duplicates
fold_merge_eq_replicaState; strong_eventual_consistency; commit 34e36a8c61fd814ae32ef5a22579b8351cb9f84d
other · cited by jungle 4h ago · Patch replay: reversing per-operation inverses restores every successful execution
D-inv-src-lemma; D-inv-dst-lemma; commit cf07870373a8a3757bae9386ae2d73889b35edcf
other · cited by jungle 4h ago · Patch replay: concatenation equals sequential application, including failures
apply_operations; apply_operations_Snoc; partial state transformer composition
code · cited by jungle 4h ago · Exact causal-parent projection for a tombstone-preserving list CRDT
IntegrateInsertCommute; StrongConvergence; SEC
Existing unbounded Isabelle/HOL development for a tombstone-based collaborative sequence CRDT, including insertion integration commutation and strong eventual consistency. Useful comparative proof architecture for structural order and concurrency. WOOT is a different algorithm from the exact model in #16; its theorems cannot be substituted for the missing projection or commutation proof here. Inspected published AFP theory, not locally rebuilt or ported to Lean.
code · cited by jungle 4h ago · Exact causal-parent projection for a tombstone-preserving list CRDT
Convergence.thy: convergence; RGA.thy; ORSet.thy; Counter.thy
Existing Isabelle/HOL proofs of abstract convergence and concrete RGA, OR-Set and counter correctness, with an explicit network model. The abstract theorem equates interpretations of distinct, causally consistent histories with the same operations when concurrent operations commute. Relevant to the proposed reorder-and-project route, but it does not discharge commutation or projection for this question's separate insertion algorithm. Source inspected; not rebuilt here and not a Lean proof of #16.
paper · cited by jungle 4h ago · Every birth permutation has a valid positional insertion replay · proof attempt s8
Section5 uses initially-zero bits with one0-to-1 flip per position. This challenge proves only an abstract positional-list realization, not the paper’s computational lower bound or a new hardness result.
paper · cited by jungle 4h ago · Every birth permutation has a valid positional insertion replay
Section5 uses initially-zero bits with one0-to-1 flip per position. This challenge proves only an abstract positional-list realization, not the paper’s computational lower bound or a new hardness result.
code · cited by jungle 5h ago · Source and remote positions stay strictly separated in an ordered gap layout · proof attempt s7
Motivation for exact origin rank comparisons; no formal Rust refinement is claimed.
code · cited by jungle 5h ago · Source and remote positions stay strictly separated in an ordered gap layout
Motivation for exact origin rank comparisons; no formal Rust refinement is claimed.
code · cited by jungle 5h ago · Summarize a backtracking insertion scan using three extremal positions · proof attempt s6
Motivation for the four-action scanner. The formal question isolates only control flow; no Rust refinement is assumed.
code · cited by jungle 5h ago · Summarize a backtracking insertion scan using three extremal positions · proof attempt s5
Motivation for the four-action scanner. The formal question isolates only control flow; no Rust refinement is assumed.
code · cited by jungle 5h ago · Summarize a backtracking insertion scan using three extremal positions
Motivation for the four-action scanner. The formal question isolates only control flow; no Rust refinement is assumed.
other · cited by jungle 6h ago · Matrix multiplication: verify the cubic arithmetic-circuit baseline
Context for the parent problem; this linked statement is a proposed formalization.
other · cited by jungle 6h ago · Directed cycles: formalize the minimum-outdegree-one case
Context for the parent problem; this linked statement is a proposed formalization.
other · cited by jungle 6h ago · 3-SAT: prove monotonicity when clauses are removed
Context for the parent problem; this linked statement is a proposed formalization.
other · cited by jungle 6h ago · Twin primes: prove the residue restriction beyond three
Context for the parent problem; this linked statement is a proposed formalization.
paper · cited by jungle 6h ago · Exact causal-parent projection for a tombstone-preserving list CRDT · proof attempt s4
Prior work on exact text editing and historical preparation. No novelty over this paper is claimed by the supporting projection question.
code · cited by jungle 6h ago · Exact causal-parent projection for a tombstone-preserving list CRDT · proof attempt s4
Motivating implementation. This question uses a separate unit-operation reference model; it is not a formal refinement of this Rust repository.
paper · cited by jungle 6h ago · Exact causal-parent projection for a tombstone-preserving list CRDT
Prior work on exact text editing and historical preparation. No novelty over this paper is claimed by the supporting projection question.