leanprover-community / leanprover-community/mathlib4
Tracking Issue: Digraph Targets
Open
@JaafarTanoukhi is already working on this.
Since Aug 12, 2025.
good first issue
t-combinatorics
- Dominant language
- Lean
- Stars
- 4.2k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
This is a list of things related to digraphs that would be nice to have.
-
Weak and strong connectivity.
- If vertices have equal in-degree and out-degree, then the digraph is weakly connected if and only if it is strongly connected.
- Robbin's Theorem.
-
Tournaments
- A tournament has a Hamiltonian path.
- A tournament has a Hamiltonian cycle If and only if it is strongly connected.
Many of the concepts that already exist in SimpleGraph should be ported to Digraph too.
Feel free to add digraph results that you would like to see formalized!
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.