RFC: proof-only import for Mandelbrot connectedness - #9
Draft
blinkybool wants to merge 3 commits into
Draft
Conversation
…import Ray/Mandelbrot.lean becomes the trusted file: it defines mandelbrot itself and authors the connectedness statements, elaborated with only its own imports active (Trustless plus three basic Mathlib modules). The proofs arrive by trustless import from the new untrusted Ray/MandelbrotBridge, which repeats the definition, proves it equals multibrot 2, and transports isConnected_multibrot across. Every imported constant is re-checked by this toolchain's kernel against the trusted file's own definitions, so the import fails unless the bridge proved exactly the statements authored here. None of the bridge's notation, instances, or macros is activated in the trusted file, and its olean is never mapped into the elaborating process: lean4export walks it in a sandboxed subprocess and only text crosses back. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kvxi5Pm1yyXH1mtDHXhEqq
Owner
|
Neat! |
The trusted files live at the package root. Mandelbrot.lean defines mandelbrot, states the two connectedness theorems, and proves each with const_fill Ray.Mandelbrot (the provider defaults to the theorem's own name). Mandelbrot2.lean is the manual comparison via const import and namespaced re-authoring. The untrusted proofs live in Ray/Mandelbrot.lean and Ray/Mandelbrot2.lean (lib RayMandelbrotSource), replacing Ray/MandelbrotBridge.lean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kvxi5Pm1yyXH1mtDHXhEqq
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
2 participants
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.
Working on a proof-only import feature at https://github.com/timaeus-research/trustless and using this as the prototype. PR still in draft state.