Hi Glauco, Please try again with new clones, I have updated some scripts. Verifying each single proof will generate the *.mm file in the target folder.
Verifying the whole project will generate *.mm file and source map files in the target folder also. ``` uv run --frozen skfd verify proof-lab ``` Best, Mingli On Thu, Feb 12, 2026 at 5:46 AM Glauco <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/1dab7fa9-5e07-43f9-81d0-22c2209b1127n%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/CAGDRuAgoCsLXq%2BBCujY4h070sOMf0uOQau9E6rHJ1pMW1%3D%3DjAw%40mail.gmail.com.
