Recover LeanVerifier v0.1 technical preview - #2
Merged
Merged
Conversation
Keep build outputs, virtualenvs, and verification scratch out of version control so recovery commits stay reviewable.
Publish STATUS, CLAIMS, and SECURITY as the authoritative preview boundary, refresh the README, and move superseded summaries and old test dumps under docs/history.
Define program ownership, review rituals, and contribution expectations so the technical preview has an explicit operating model.
Replace the old lakefile with a pinned preview toolchain and a minimal LeanVerifier library root built around a typed Vector datatype.
Encode the binary affine classifier semantics that the v0.1 technical preview can generate proofs about.
Formalize classification robustness on L-infinity balls, prove the affine margin theorem, and expose the audited public axiom surface.
Define the exchange formats for models, requests, and results so the generator and Lean artifacts share one contract.
Provide canonicalization, manifest handling, and deterministic Lean generation for the AffineBinary preview path.
Expose verify and related commands so users can drive schema validation and Lean generation from the shell.
Cover generator determinism, schema conformance, CLI flows, mutation resistance, and basic security guards for the preview toolchain.
Quarantine the prior lean/translator/webapp surface so it is clearly non-authoritative while recovering the v0.1 LeanVerifier preview.
Spell out what the technical preview claims, what it does not, and how releases are reproduced and reviewed.
Wire preview checks and RC packaging so builds, dependency updates, and release reproduction have a single supported path.
Drop committed .lake outputs and package gitlinks, and replace the obsolete Lean-only workflow with the new CI layout.
Record recoverable release notes and a citable metadata record for the technical preview.
Rewrite the guides around LeanVerifier v0.1 scope so onboarding matches STATUS and the new package layout.
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
experimental/legacy-formalverifml.lean_ciwith gitignore, CI/Dependabot, Docker, and release-RC scaffolding, plus CHANGELOG/CITATION.Test plan
lake buildsucceeds on the pinnedlean-toolchainpip install -e .[dev](or project equivalent) andpytestpassexamples/affine_binaryscripts/audit_axioms.py/scripts/verify_docs.pyas documented