Hi Mingli, I've tried it in Play-With-Docker, here is the script that worked for me (from a clean new PWD instance):
curl -LsSf https://astral.sh/uv/install.sh | sh source $HOME/.local/bin/env git clone https://github.com/epistemic-frontier/metamath-logic.git git clone https://github.com/epistemic-frontier/metamath-prelude.git git clone https://github.com/epistemic-frontier/proof-lab.git cd proof-lab uv run skfd verify prove_modus_tollens.py here's the output [node1] (local) [email protected] ~/proof-lab $ uv run --frozen skfd verify prove_modus_tollens.py Verifying script: prove_modus_tollens.py ... Found 1 proof(s): prove_modus_tollens Running prove_modus_tollens... OK (modus_tollens) Emitting 1 proofs to Metamath... OK Is the proof stored somewhere? Glauco Il giorno mercoledì 11 febbraio 2026 alle 21:32:18 UTC+1 [email protected] ha scritto: > Hi Glauco, > > I saw your email and felt very inspired. So I worked late this night to > make the code ready. > > Now I have published metamath-prelude and metamath-logic. They are still > "alpha" versions and not perfect, but I think they are usable now. > > *1. Proof Lab* I made a new repo called *Proof Lab* here: > https://github.com/epistemic-frontier/proof-lab > > You can clone it and just follow the README. It can verify the Python > proofs (like your mp2 example) using the real Metamath verifier. > > *2. Original Authorship* Also, I want to say one thing. Even though I use > a Python interface, I try my best to keep the original author's comments in > the source code. For example, please check this file: > https://github.com/epistemic-frontier/metamath-logic/blob/main/src/logic/propositional/hilbert/lemmas.py#L222 > > You can see the note from *NM (Norman Megill) on 30-Sep-1992* is kept > there. I think attribution is very important. > > Please try the lab. Let me know if you have any problems. > > Best, > > Mingli > > On Wed, Feb 11, 2026 at 10:33 PM Mingli Yuan <[email protected]> wrote: > >> Hi Glauco, >> >> Thanks for checking. >> >> Logically, the structure is correct: from φ and (φ → (ψ → χ)) we get (ψ → >> χ) by MP, then from ψ we get χ by MP again. So the *proof skeleton* is >> right. >> >> However, my porting work is not finished yet, the >> logic.propositional.hilbert and related packages are not released yet, >> so this code can not be verified by the community right now. There are >> around 20k lines of proofs in the logic part of metamath, please give me >> some time to finish it. >> >> Or, I may release the prelude and logic package earlier before it is >> fully ported, if anyone is interested. >> >> Best, >> >> Mingli >> >> On Wed, Feb 11, 2026 at 9:07 PM Glauco <[email protected]> wrote: >> >>> Hi Mingli Yuan, >>> >>> I've given Gemini your README.md and asked it to prove mp2 with your >>> framework. Below is the Python code that Gemini returned. >>> Is it completely hallucinated, or is it close? >>> >>> from logic.propositional.hilbert import System >>> from logic.propositional.hilbert.lemmas import Proof, ProofBuilder >>> >>> def prove_mp2(sys: System) -> Proof: >>> """ >>> Double Modus Ponens: φ, ψ, (φ → (ψ → χ)) ⊢ χ >>> """ >>> # 1. Initialize the builder with the system and theorem name >>> lb = ProofBuilder(sys, "mp2") >>> >>> # 2. Define Hypotheses (mp2.1, mp2.2, mp2.3) >>> h_phi = lb.hyp("mp2.1", "φ") >>> h_psi = lb.hyp("mp2.2", "ψ") >>> h_chi_nested = lb.hyp("mp2.3", "φ → (ψ → χ)") >>> >>> # 3. Apply the first Modus Ponens (Step 4 in .mmp) >>> # This uses h_phi and h_chi_nested to get (ψ → χ) >>> step4 = lb.mp("s1", h_phi, h_chi_nested, note="Step 4: MP h_phi, >>> h_chi_nested") >>> >>> # 4. Apply the second Modus Ponens (Step 5 in .mmp) >>> # This uses h_psi and step4 to get χ >>> step5 = lb.mp("s2", h_psi, step4, note="Step 5: MP h_psi, s1") >>> >>> # 5. Return the build targeting the final result >>> return lb.build(step5) >>> >>> BR >>> Glauco >>> >>> Il giorno mercoledì 11 febbraio 2026 alle 08:05:05 UTC+1 >>> [email protected] ha scritto: >>> >>>> Dear Metamath Community, >>>> >>>> I am writing to share an open-source project we have been working on >>>> called ProofScaffold ( >>>> https://github.com/epistemic-frontier/proof-scaffold). >>>> >>>> Our team has deep respect for set.mm and the rigorous foundation this >>>> community has built. However, as we explore the intersection of Metamath >>>> and Large Language Models (LLMs), we’ve encountered a persistent >>>> challenge: >>>> feeding a 48MB monolithic file to an AI often leads to context dilution, >>>> hallucinated imports, and noisy proof searches. >>>> >>>> To solve this, we built ProofScaffold. It acts as a package manager and >>>> linker (written in Python) for Metamath. It allows us to split massive >>>> databases into composable, compilable, and independently verifiable >>>> packages with explicit dependencies and exports—much like Cargo or NPM, >>>> but >>>> for formal math. >>>> >>>> Crucially, the Trust Computing Base (TCB) does not change. Python acts >>>> strictly as an untrusted builder/linker. The final output is a standard, >>>> flattened .mm transient monolith that is verified by metamath-exe or >>>> metamath-knife. >>>> >>>> We believe this modularity is the key to unlocking AI's true potential >>>> in formal mathematics: >>>> >>>> - Targeted Retrieval: By scoping the context to a specific package >>>> (e.g., just fol or zf), we drastically reduce noise for the LLM. >>>> >>>> - Controlled Semantic Boundaries: Explicit exports provide the AI with >>>> a strict subset of permissible symbols and axioms. This prevents >>>> hallucinated reasoning, such as an AI accidentally employing the Axiom of >>>> Choice in a strict ZF-only context. >>>> >>>> - Verifiable Incremental Loops: An AI can generate a proof, verify it >>>> locally within the package, and map any verifier errors directly back to >>>> the specific package contract (e.g., missing $f or label conflicts). This >>>> makes AI self-correction much more reliable. >>>> >>>> - Curriculum Alignment: Modular packages naturally form a curriculum >>>> (axioms → definitions → lemmas → theorems), providing high-quality >>>> gradient >>>> data for training models, rather than overwhelming them with the entire >>>> set.mm at once. >>>> >>>> We have successfully ported a prelude and are currently porting the >>>> logic package (aligned with the |- conventions of set.mm). Our next >>>> step is to further subdivide logic into prop, fol, eq, and setvar >>>> packages, >>>> and to generate machine-readable interface manifests to help AI planners. >>>> >>>> A Question for the Community regarding PyPI Naming: >>>> >>>> To make this ecosystem easily accessible for AI researchers and >>>> engineers, we plan to publish these modularized databases as Python >>>> packages on PyPI. >>>> >>>> I would like to ask if the community is comfortable with us using the >>>> metamath- prefix for these packages (e.g., metamath-logic, metamath-zfc). >>>> I >>>> want to be entirely respectful of the Metamath trademark/legacy and ensure >>>> this doesn't cause confusion with official tools. If the community prefers >>>> we use a different namespace (e.g., proof-scaffold-logic), we will gladly >>>> do so. >>>> >>>> I would love to hear your thoughts, feedback, or critiques on this >>>> approach. >>>> >>>> Best regards, >>>> >>>> Mingli Yuan >>>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Metamath" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> To view this discussion visit >>> https://groups.google.com/d/msgid/metamath/6caee51b-6405-4a23-837e-8d47339b5df7n%40googlegroups.com >>> >>> <https://groups.google.com/d/msgid/metamath/6caee51b-6405-4a23-837e-8d47339b5df7n%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/1dab7fa9-5e07-43f9-81d0-22c2209b1127n%40googlegroups.com.
