Skip to content

feat: add support for disproofs - #16

Merged
GasStationManager merged 5 commits into
GasStationManager:mainfrom
Paul-Lez:disproofs
Apr 22, 2026
Merged

feat: add support for disproofs#16
GasStationManager merged 5 commits into
GasStationManager:mainfrom
Paul-Lez:disproofs

Conversation

@Paul-Lez

@Paul-Lez Paul-Lez commented Feb 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR adds support for disproof submissions: when a target file contains a theorem foo, a submission file may instead provide foo.disproof (a proof of the negation of foo's statement) rather than a proof of foo itself.

This is useful in challenge settings where the target statement may be false and contestants should demonstrate this by proving its negation.

More specifically this does the following:

  • Adds a --disproofs CLI flag to opt in to disproof checking
  • Adds allowDisproofs : Bool to Settings and env : Environment to Decls (needed to run the negation check)
  • Adds checkNegatedTheorem in Util.lean, which checks that a submission's type is definitionally equal to the negation of the target's type
  • checkTargets now looks for a foo.disproof entry in the submission when allowDisproofs is set, and routes it through the negation check instead of the standard type-equality check

@Paul-Lez
Paul-Lez force-pushed the disproofs branch 2 times, most recently from df47833 to 28aabf3 Compare April 12, 2026 13:48
@henrykmichalewski henrykmichalewski mentioned this pull request Apr 13, 2026
Merged
3 of 4 tasks
@GasStationManager
GasStationManager merged commit b291b58 into GasStationManager:main Apr 22, 2026
1 check failed
@GasStationManager GasStationManager mentioned this pull request Apr 22, 2026
Open
mo271 pushed a commit to wcook04/formal-conjectures that referenced this pull request Sep 18, 2026
@henrykmichalewski
Disproof of Mukwembi's Theorem 2.1 via Q₃ (3-cube) (google-deepmind#3726
491adb1 
)

## Summary

- Formal disproof of Theorem 2.1 from Mukwembi, *Size, Order, and
Connected Domination*, Canad. Math. Bull. **57** (2014), 141–144
- The 3-dimensional hypercube Q₃ is a counterexample: n=8, m=12, γ_c=4,
bound=11 < 12
- The paper's proof (p. 143) asserts γ_c(G) ≤ γ_c(G − {u,v}) without
justification; this is false for Q₃ where γ_c(G') = 2 < 4 = γ_c(Q₃) for
every edge
- Corollaries 2.2 and 2.3 remain true (proved independently via
`GraphConjecture2.lean`)

## Files

| File | Description |
|------|-------------|
| `Q3Counterexample.lean` | Full Lean 4 proof: γ_c(Q₃) = 4,
triangle-free, 12 > 11 |
| `Q3SafeVerifyTarget.lean` | SafeVerify target: Mukwembi's bound with
`sorry` |
| `Q3SafeVerifySubmission.lean` | SafeVerify disproof: negation proved
without `native_decide` |
| `SizeOrderConnectedDomination.lean` | Lemma 1.2, Eq (1.1), Cor 2.2,
Cor 2.3 |
| `COUNTEREXAMPLE.md` | Detailed writeup with proof gap analysis |
| `COUNTEREXAMPLE.pdf` | PDF version |
| `Q3_counterexample.py` | Computational verification |

## SafeVerify disproof verification

Verified using SafeVerify's `--disproofs` mode
([GasStationManager/SafeVerify#16](GasStationManager/SafeVerify#16)):
- `mukwembi_size_bound.disproof` proves ∃ G, Connected G ∧ CliqueFree 3
G ∧ ¬(m ≤ bound)
- All 26 declarations replayed, only standard axioms used
- `SafeVerify check passed.`

## Test plan

- [x] `Q3Counterexample.lean` compiles with `lake build` (57s, uses
`native_decide`)
- [x] `Q3SafeVerifySubmission.lean` compiles (no `native_decide`, uses
`decide` with increased limits)
- [x] SafeVerify `--disproofs` check passes
- [ ] CI build on upstream

🤖 Generated with [Claude Code](https://claude.com/claude-code)
felixpernegger pushed a commit to felixpernegger/formal-conjectures that referenced this pull request Oct 14, 2026
@henrykmichalewski @felixpernegger
Disproof of Mukwembi's Theorem 2.1 via Q₃ (3-cube) (google-deepmind#3726
3dae2e3 
)

## Summary

- Formal disproof of Theorem 2.1 from Mukwembi, *Size, Order, and
Connected Domination*, Canad. Math. Bull. **57** (2014), 141–144
- The 3-dimensional hypercube Q₃ is a counterexample: n=8, m=12, γ_c=4,
bound=11 < 12
- The paper's proof (p. 143) asserts γ_c(G) ≤ γ_c(G − {u,v}) without
justification; this is false for Q₃ where γ_c(G') = 2 < 4 = γ_c(Q₃) for
every edge
- Corollaries 2.2 and 2.3 remain true (proved independently via
`GraphConjecture2.lean`)

## Files

| File | Description |
|------|-------------|
| `Q3Counterexample.lean` | Full Lean 4 proof: γ_c(Q₃) = 4,
triangle-free, 12 > 11 |
| `Q3SafeVerifyTarget.lean` | SafeVerify target: Mukwembi's bound with
`sorry` |
| `Q3SafeVerifySubmission.lean` | SafeVerify disproof: negation proved
without `native_decide` |
| `SizeOrderConnectedDomination.lean` | Lemma 1.2, Eq (1.1), Cor 2.2,
Cor 2.3 |
| `COUNTEREXAMPLE.md` | Detailed writeup with proof gap analysis |
| `COUNTEREXAMPLE.pdf` | PDF version |
| `Q3_counterexample.py` | Computational verification |

## SafeVerify disproof verification

Verified using SafeVerify's `--disproofs` mode
([GasStationManager/SafeVerify#16](GasStationManager/SafeVerify#16)):
- `mukwembi_size_bound.disproof` proves ∃ G, Connected G ∧ CliqueFree 3
G ∧ ¬(m ≤ bound)
- All 26 declarations replayed, only standard axioms used
- `SafeVerify check passed.`

## Test plan

- [x] `Q3Counterexample.lean` compiles with `lake build` (57s, uses
`native_decide`)
- [x] `Q3SafeVerifySubmission.lean` compiles (no `native_decide`, uses
`decide` with increased limits)
- [x] SafeVerify `--disproofs` check passes
- [ ] CI build on upstream

🤖 Generated with [Claude Code](https://claude.com/claude-code)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@GasStationManager GasStationManager GasStationManager approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Paul-Lez @GasStationManager