Skip to content

doc: add wikidata attributes - #42608

Open
Deicyde wants to merge 1 commit into
leanprover-community:masterfrom
Deicyde:wikilean/wikidata-batch-7
Open

doc: add wikidata attributes#42608
Deicyde wants to merge 1 commit into
leanprover-community:masterfrom
Deicyde:wikilean/wikidata-batch-7

Conversation

@Deicyde

@Deicyde Deicyde commented Aug 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR adds a batch of 6 @[wikidata] attributes.

Claude helped generate the list of crossrefs (by scanning Wikidata + Mathlib). Comments are generated by crossref-report and Wikilean.

See https://wikilean.jackmccarthy.org/review?pr=42608 for reviewer UI.

@Deicyde

Deicyde commented Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

This PR adds 5 @[wikidata] cross-reference tags.

# Concept Wikidata Mathlib declaration Reviews
1 Induced subgraph Q24743362 SimpleGraph.Subgraph.induce —
2 Set (mathematics) Q36161 Set —
3 Inequality (mathematics) Q28113351 LinearOrder —
4 Partially ordered set Q474715 PartialOrder —
5 Zermelo–Fraenkel set theory Q191849 ZFSet —

Reviews: 🟢 approve · 🟡 revise · 🔴 reject · ⚠️ deletion-candidate · 💬 comment. * = maintainer. Recycled tags: https://wikilean.jackmccarthy.org/queue

@Deicyde

Deicyde commented Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

LLM-generated

Deicyde
Deicyde commented Aug 10, 2026
View reviewed changes
Comment thread Mathlib/SetTheory/ZFC/Basic.lean Outdated
Comment on lines 48 to 49
@[pp_with_univ, use_set_notation_for_order, wikidata Q191849]
def ZFSet : Type (u + 1) :=

@Deicyde Deicyde Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wikidata Q191849: Zermelo–Fraenkel set theory — variant of ZFC, the standard axiomatic set theory

Comment thread Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
Comment on lines +1172 to 1173
@[simps, wikidata Q24743362]
def induce (G' : G.Subgraph) (s : Set V) : G.Subgraph where

@Deicyde Deicyde Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wikidata Q24743362: induced subgraph — another graph, formed from a subset of the vertices of the graph and all of the edges connecting pairs of vertices in that subset

@SnirBroshi SnirBroshi Aug 10, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As I've mentioned before, SimpleGraph.induce fits better (this is SimpleGraph.Subgraph.induce) but they should probably both be tagged.

Comment thread Mathlib/Order/Defs/LinearOrder.lean Outdated
Comment on lines 62 to 63
@[wikidata Q28113351]
class LinearOrder (α : Type*) extends PartialOrder α, Min α, Max α, Ord α where

@Deicyde Deicyde Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wikidata Q28113351: inequality — mathematical relation comparing two different values

Comment thread Mathlib/Data/Set/Defs.lean Outdated
Comment on lines 51 to 52
@[use_set_notation_for_order, wikidata Q36161, wikidata Q903783]
def Set (α : Type u) := α → Prop

@Deicyde Deicyde Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wikidata Q36161: set — well-defined mathematical collection of distinct objects

Comment thread Mathlib/Order/Defs/PartialOrder.lean Outdated
Comment on lines 179 to 180
@[wikidata Q474715]
class PartialOrder (α : Type*) extends Preorder α where

@Deicyde Deicyde Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wikidata Q474715: partially ordered set — set ordered by a transitive, antisymmetric, and reflexive binary relation

@SnirBroshi SnirBroshi Aug 10, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you also add Q1069998 (partial order)?
To emphasize, I think both do belong here, even though the set version seems a bit weird.

Comment thread Mathlib/Data/Set/Defs.lean Outdated
Comment on lines 51 to 52
@[use_set_notation_for_order, wikidata Q36161, wikidata Q903783]
def Set (α : Type u) := α → Prop

@Deicyde Deicyde Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wikidata Q903783: naive set theory — one of several theories of sets used in the discussion of the foundations of mathematics; defined informally, in natural language

@github-actions github-actions Bot added the LLM-generated PRs with substantial input from LLMs - review accordingly label Aug 10, 2026
@github-actions

github-actions Bot commented Aug 10, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 59a4f00bda

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 59a4f00).

  • +0 new declarations
  • −0 removed declarations

No declaration differences.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 59a4f00bda
Reference commit 3b5417e200

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

@Deicyde
Deicyde force-pushed the wikilean/wikidata-batch-7 branch 6 times, most recently from 50933f3 to bb4c32d Compare August 11, 2026 22:46
@Deicyde
Deicyde force-pushed the wikilean/wikidata-batch-7 branch from bb4c32d to 59a4f00 Compare August 12, 2026 01:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer
@SnirBroshi SnirBroshi SnirBroshi left review comments
Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

LLM-generated PRs with substantial input from LLMs - review accordingly

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Deicyde @SnirBroshi