feat(Combinatorics): define undirected hypergraphs by espottesmith · Pull Request #28613 · leanprover-community/mathlib4

espottesmith · 2025-08-18T21:03:23Z

This PR defines undirected hypergraphs:

@[ext]
structure Hypergraph (α : Type*) where
  /-- The vertex set -/
  vertexSet : Set α
  /-- The hyperedge set -/
  hyperedgeSet : Set (Set α)
  /-- All hyperedges must be subsets of the vertex set -/
  hyperedge_isSubset_vertexSet : ∀ ⦃e⦄, e ∈ hyperedgeSet → e ⊆ vertexSet

In addition to the main definition, some additional definitions and related lemmas are provided:

vertex adjacency
hyperedge adjacency
vertex "stars"
special cases (loops, empty hypergraphs, trivial hypergraphs, complete hypergraphs, simple hypergraphs, k-uniform hypergraphs, and d-regular hypergraphs)
(some) hypergraph cardinality
subhypergraphs, induced subhypergraphs, and partial hypergraphs

This implementation is certainly bare-bones. I'm submitting this PR at this point, rather than when my developments are more fleshed out, because there has been some interest in others contributing to hypergraph formalization in mathlib.

In the near future, goals include:

defining incidence matrices (i.e., conversion from Hypergraph α to Matrix α (Set α) β
coersion/generalization of graph as 2-uniform hypergraph
conversion of a hypergraph into its associated clique graph/two-section graph
constructing the dual of a hypergraph (note: on first blush, this appears somewhat challenging, given that we define hyperedges as Set α rather than some other type β)
rank and co-rank
walks, paths, cycles, etc. on hypergraphs

to need to reimplement a lot of stuff

much of the work

first...

simpler

github-actions · 2025-08-18T21:04:35Z

PR summary 2e36a1dbb4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.Hypergraph.Basic` (new file)	742

Declarations diff

+ Adj
+ Adj.symm
+ EAdj
+ EAdj.exists_vertex
+ EAdj.inter_nonempty
+ EAdj.symm
+ Hypergraph
+ IsComplete
+ IsEmpty
+ IsEmpty.eq
+ IsEmpty.not_isNonempty
+ IsEmpty.not_mem
+ IsIsolated
+ IsLoop
+ IsNonempty
+ IsNonempty.not_isEmpty
+ IsTrivial
+ _root_.Membership.mem.subset_vertexSet
+ adj_comm
+ coe_nonempty
+ completeOn
+ completeOn_isNonempty
+ completeOn_not_isTrivial
+ eAdj_comm
+ edgeSet_subset_powerset_vertexSet
+ edge_isSubset_vertexSet
+ edge_not_mem_empty
+ edge_not_mem_trivial
+ emptyHypergraph
+ forall_of_forall_verts
+ image
+ image_image
+ image_mem_image
+ isComplete_completeOn
+ isComplete_not_isEmpty
+ isComplete_not_isTrivial
+ isEmpty_empty_hypergraph
+ isEmpty_eq_empty_hypergraph
+ isEmpty_iff_forall_not_mem
+ isEmpty_or_isNonempty
+ isLoop_encard_one
+ mem_completeOn
+ mem_image
+ mem_vertexSet_of_mem_edgeSet
+ not_exists_isolated_vertex_iff_sUnion_edgeSet_eq_vertexSet
+ not_isEmpty
+ not_isEmpty_trivial_hypergraph
+ not_isNonempty
+ sUnion_edgeSet_subset_vertexSet
+ star
+ stars
+ trivialHypergraph

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib4-merge-conflict-bot · 2025-08-28T21:55:15Z

This pull request has conflicts, please merge master and resolve them.

b-mehta · 2025-09-02T16:19:38Z

Just to note that this is marked awaiting-author for the comments above, once those are fixed you can remove the tag by commenting "-awaiting-author".

jt496

This looks good. It will be great to have Hypergraphs in mathlib!

I know this was already raised but I also prefer "edgeSet" to "hyperedgeSet" on the basis that "hyperedges" are almost always referred to as "edges" and it will make theorem names a little shorter. (Also why E(H) if they are hyperedges?)

Mathlib/Combinatorics/Hypergraph/Basic.lean

espottesmith · 2025-09-04T15:16:19Z

Thanks for the heads up, @b-mehta. I still wanted to look a bit more deeply into using simp, as @lauramonk had suggested, before I claimed to be totally done.

And thanks for your comments, @jt496. I disagree that hyperedges are usually called edges (at least in the papers I read, they're frequently referred to as "hyperedges", even if the E(H) notation is used). But, since multiple folks have brought this up, I'm happy acquiescing.

proofs

espottesmith · 2025-09-05T10:26:44Z

-awaiting-author

mathlib4-merge-conflict-bot · 2025-11-19T07:57:44Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-merge-conflict-bot · 2025-12-10T07:54:12Z

This pull request has conflicts, please merge master and resolve them.

Might this help?

espottesmith added 26 commits August 5, 2025 18:57

First steps towards formal hypergraphs

5a17479

Mostly still working on definitions; should be ready for feeedback soon

2f0e2e9

Small formatting tweaks & comments

4b42a61

More definitions

06a9510

Merge remote-tracking branch 'lean/master' into undirhyper

4c56d5c

Still in definition world

4806191

File rename

2875013

Trying a more rigorous definition with some requirements included; going

0949334

to need to reimplement a lot of stuff

Delete simple definitions (e.g., empty hypergraph) because predicates do

ae2fc95

much of the work

Reorganizaing

d7d76ea

Some work on dual. I think I'm going to need to write a lot of lemmas

b64e9ed

first...

Merge remote-tracking branch 'lean/master' into undirhyper

0d13081

Some definition tweaking

1a81825

New implementation in progress; duals seem awkward, but otherwise

74fce35

simpler

New implementation; definitions (mostly) done (some small holes)

00876ca

Getting to work on some lemmas

213e5c7

Probably tedious and longwinded definition of subhypergraph

2a17272

Induced sub-hypergraph

36f4d26

Partial hypergraph

6db564c

Whoops; didn't save

f7391ec

Some work on empty hypergraphs, preliminary work on extensionality

3571bdc

Small but necessary tweak to EAdj; some more small lemmas

3f4202c

Merge remote-tracking branch 'lean/master' into undirhyper

65a0883

Clean up; ready for PR?

fecdba3

Merge remote-tracking branch 'lean/master' into undirhyper

c9478f9

One unused variable

57c6335

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics labels Aug 18, 2025

Fix CI

1a7c367

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 24, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 28, 2025

Merge remote-tracking branch 'lean/master' into undirhyper

3cf358a

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 29, 2025

jt496 reviewed Sep 2, 2025

View reviewed changes

espottesmith added 6 commits September 4, 2025 16:17

Merge remote-tracking branch 'lean/master' into undirhyper

f74ec16

Amendments made in response to review comments; shortedned a bunch of

2a877d2

proofs

Unnecessary (I think?) imports

80f5c19

Trying to add more @[simp] lemmas...

7add493

Fix issues with simp lemmas, slightly restructure EAdj

ac0b19b

Make the linter happy

20e980e

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 5, 2025

espottesmith mentioned this pull request Sep 17, 2025

feat(Combinatorics): define directed hypergraphs #29744

Open

cosmicgenius mentioned this pull request Sep 26, 2025

Erdős Problem 712 - Turán Numbers of Complete Hypergraphs google-deepmind/formal-conjectures#690

Open

2 tasks

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

Merge branch 'master' into undirhyper

0df96a0

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

Merge branch 'master' into undirhyper

3426775

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 10, 2025

Merge branch 'master' into undirhyper

6ced214

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 3, 2026

espottesmith and others added 3 commits April 3, 2026 09:40

Slight import changes

b227cca

Public and private stuff has changed since I was last mucking about.

c273448

Might this help?

Merge branch 'master' into undirhyper

3a80789

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Combinatorics): define undirected hypergraphs#28613

feat(Combinatorics): define undirected hypergraphs#28613
espottesmith wants to merge 61 commits intoleanprover-community:masterfrom
espottesmith:undirhyper

espottesmith commented Aug 18, 2025

Uh oh!

github-actions bot commented Aug 18, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Aug 28, 2025

Uh oh!

b-mehta commented Sep 2, 2025

Uh oh!

jt496 left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

espottesmith commented Sep 4, 2025

Uh oh!

espottesmith commented Sep 5, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Dec 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

espottesmith commented Aug 18, 2025

Uh oh!

github-actions bot commented Aug 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2e36a1dbb4

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Aug 28, 2025

Uh oh!

b-mehta commented Sep 2, 2025

Uh oh!

jt496 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

espottesmith commented Sep 4, 2025

Uh oh!

espottesmith commented Sep 5, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Dec 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented Aug 18, 2025 •

edited

Loading