Öffentliches RegisterGefährdet
Software-GesundheitsberichtSchema 0.27.0 · Metriken 1.13.0 · 2026-07-27 22:19 UTC
mattrobball / mathlib4_fork
The math library of Lean 4
mattrobball/mathlib4_fork erreicht einen Gesundheitsindex von 37 von 100 und liegt damit im Bereich Gefährdet. Am stärksten schneidet es bei Sustainability & Governance (75/100) ab, am schwächsten bei Community & Adoption (12/100). Zuletzt vor 129 Tagen aktualisiert. 12 Mitwirkende tragen den Großteil der jüngsten Arbeit.
37
gesamt / 100Software-Gesundheitsindex
Metriken werden auf einer Skala von 1–100 in gewichtete Kategorien gruppiert. Der Gesamtwert beginnt als ihr Mittel; sobald öffentliche Evidenz die Richtlinie für Hochrisikojurisdiktionen auslöst, wird die Bewertung angepasst und erhält die Obergrenze 49 (Gefährdet). AI Readiness liegt außerhalb.
37
Exzellent85-100Vorbildlich; erfüllt im Wesentlichen alle geprüften Kriterien
Gut70-84Gesund; geringfügige Lücken
Mittel50-69Akzeptabel mit deutlichen Lücken; Überprüfung empfohlen
Gefährdet30-49Erhebliche Schwächen; eine Übernahme erfordert Vorsicht
Kritisch1-29Schwerwiegende Probleme (aufgegeben, nur ein Maintainer, keine Hygiene)
Bewertungsprofil
Jede Achse ist eine Kategorie. Die Form zählt mehr als der Durchschnitt — ein gesundes Projekt füllt die gesamte Fläche, während ein Profil aus Spitzen und Kratern bedeutet, dass Stärke in einer Dimension Risiken in einer anderen verdeckt.
Abandonment Policy applies a 85% multiplier to weighted overall health.
Eigentümerschaft
Matthew Robert BallardPersönliches Konto
24 Follower37 öffentliche Reposseit Feb. 2022@ICARM
Dieses Repository gehört einem persönlichen Konto. Ein Projekt mit nur einem Eigentümer trägt ein höheres Kontinuitätsrisiko als ein organisationsgetragenes.
Metriken nach Kategorie
Vitalität
Lebt das Projekt — wird Code geschrieben und werden Releases ausgeliefert?
28
Entwicklungsaktivität
10Kritisch
Hinweis auf Verwaisung
Arbeit ist eingegangen, und niemand hat sich darum gekümmert
seit 411 Tagen kein menschlicher Commitautomatisierte Commits ausgenommenReleases stehen stillOpenSSF Scorecard meldet es als ungepflegt
Stille allein ist nie der Befund — eine kleine, fertige Bibliothek braucht womöglich jahrelang keinen Commit. Dieser Hinweis verlangt beides: lange keinen menschlichen Commit und Pflichten, denen das Projekt sichtbar nicht nachkommt. Automatisierte Commits gelten nicht als Pflege.
Wie Verwaisung bewertet wirdWie die Bewertung erfolgt
| 9.9/36 | Push-Aktualität — letzter Push vor 129 Tagen |
| 0/36 | Commit-Rhythmus — 0/52 Wochen mit Commits |
| 0/18 | Commit-Volumen — 0 Commits im letzten Jahr |
| 0/10 | OpenSSF Scorecard: Maintained — 0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0 |
Verwendete Eingangsdaten
| commits_last_year | 0 |
| human_commit_share | 0,97 |
| days_since_last_push | 129 |
| active_weeks_last_year | 0 |
Release-Disziplin
56Mittel
Wie die Bewertung erfolgt
| 16.2/27 | Liefert Releases aus — 14 Versions-Tags (keine GitHub-Releases) |
| 7.2/36 | Release-Aktualität — letztes Release vor 418 Tagen |
| 27/27 | Release-Rhythmus — ein Release etwa alle 5,8 Tage |
| 0/10 | OpenSSF Scorecard: Signed-Releases — keine Daten |
Verwendete Eingangsdaten
| releases_count | 14 |
| latest_release_tag | v4.20.1 |
| releases_from_tags | ja |
| days_since_latest_release | 418 |
| mean_days_between_releases | 5,8 |
Von der Bewertung ausgeschlossen (keine Daten oder nicht anwendbar): OpenSSF Scorecard: Signed-Releases. Die verbleibenden Gewichte wurden renormalisiert.
Community & Verbreitung
Hat das Projekt Nutzer, Downloads, Aufmerksamkeit und ein einladendes Umfeld für Beitragende?
12
Popularität & Verbreitung
1Kritisch
Wie die Bewertung erfolgt
| 0/60 | Stars — 0 Stars |
| 0/25 | Forks — 0 Forks |
| 0/15 | Watcher — 0 Watcher |
Verwendete Eingangsdaten
| forks | 0 |
| stars | 0 |
| watchers | 0 |
| growth_state | unverified |
| growth_factor_pct | 100 |
| growth_unverified_reason | no_history |
Community-Gesundheit
25Kritisch
Wie die Bewertung erfolgt
| 0/22.5 | README |
| 22.5/22.5 | Lizenz — anerkannte Lizenz (Apache-2.0) |
| 0/18 | CONTRIBUTING-Leitfaden |
| 0/13.5 | Verhaltenskodex |
| 0/7.2 | Issue-Vorlage |
| 0/6.3 | PR-Vorlage |
Verwendete Eingangsdaten
| has_readme | nein |
| has_license | nein |
| has_contributing | nein |
| has_issue_template | nein |
| has_code_of_conduct | nein |
| has_pull_request_template | nein |
Nachhaltigkeit & Governance
Überdauert das Projekt die Menschen, die es tragen — Bus-Faktor, Reaktionsfähigkeit, Trägerschaft und Paketpflege?
75
Maintainer-Resilienz (Bus-Faktor)
98Exzellent
Wie die Bewertung erfolgt
| 54/54 | Bus-Faktor — 12 Beitragende decken die Hälfte aller Commits ab |
| 20.5/22.5 | Commit-Verteilung — wichtigste beitragende Person verfasste 9 % der Commits |
| 13.5/13.5 | Breite der Beitragenden — 99 Beitragende |
| 10/10 | OpenSSF Scorecard: Contributors — project has 35 contributing companies or organizations |
Verwendete Eingangsdaten
| bus_factor | 12 |
| contributors_sampled | 99 |
| top_contributor_share | 0,088 |
Wie die Bewertung erfolgt
| 0/46.8 | Issue-Lösungsquote — keine Issues oder keine Daten |
| 38.2/38.3 | PR-Annahme — 1/1 entschiedene PRs gemergt |
| 0/15 | OpenSSF Scorecard: Code-Review — Found 0/30 approved changesets -- score normalized to 0 |
Verwendete Eingangsdaten
| merged_prs | 1 |
| open_issues | 0 |
| closed_issues | 0 |
| issue_closed_ratio | — |
| closed_unmerged_prs | 0 |
Von der Bewertung ausgeschlossen (keine Daten oder nicht anwendbar): Issue-Lösungsquote. Die verbleibenden Gewichte wurden renormalisiert.
Eigentümerschaft & Trägerschaft
51Mittel
Wie die Bewertung erfolgt
| 10/30 | Organisatorische Trägerschaft — persönliches (Nutzer-)Konto |
| 0/20 | Verifizierte Domain — für Nutzerkonten nicht anwendbar |
| 10.1/25 | Reichweite des Inhabers — 24 Follower von mattrobball |
| 20.4/25 | Kontohistorie — 37 öffentliche Repos, Kontoalter ca. 4 Jahre |
Verwendete Eingangsdaten
| followers | 24 |
| owner_type | User |
| is_verified | — |
| owner_login | mattrobball |
| public_repos | 37 |
| account_age_days | 1.619 |
Von der Bewertung ausgeschlossen (keine Daten oder nicht anwendbar): Verifizierte Domain. Die verbleibenden Gewichte wurden renormalisiert.
Engineering-Qualität
Sind grundlegende Engineering- und Dokumentationspraktiken vorhanden?
56
Engineering-Praktiken
60Mittel
Wie die Bewertung erfolgt
| 24/24 | CI-Workflows — 32 Workflow(s) |
| 24/24 | Tests vorhanden |
| 0/16 | Linter-Konfiguration |
| 0/9.6 | Pre-Commit-Hooks |
| 0/6.4 | .editorconfig |
| 0/20 | OpenSSF Scorecard: CI-Tests — keine Daten |
Verwendete Eingangsdaten
| has_ci | ja |
| has_tests | ja |
| has_editorconfig | nein |
| has_linter_config | nein |
| has_precommit_config | nein |
Von der Bewertung ausgeschlossen (keine Daten oder nicht anwendbar): OpenSSF Scorecard: CI-Tests. Die verbleibenden Gewichte wurden renormalisiert.
Dokumentation
50Mittel
Wie die Bewertung erfolgt
| 0/30 | README |
| 25/25 | Dokumentationsverzeichnis |
| 15/15 | Dokumentations-/Homepage-Site — https://leanprover-community.github.io/mathlib4_docs |
| 0/10 | Repository-Beschreibung |
| 0/10 | Topics |
| 10/10 | Wiki |
Verwendete Eingangsdaten
| topics | — |
| has_wiki | ja |
| homepage | https://leanprover-community.github.io/mathlib4_docs |
| has_readme | nein |
| has_docs_dir | ja |
| has_description | nein |
Sicherheit
Sind die sichtbaren Sicherheits- und Lieferkettenpraktiken belastbar, ohne ungeklärte Exposition gegenüber Hochrisikojurisdiktionen?
38
Sicherheitslage
38Gefährdet
Wie die Bewertung erfolgt
| 7.5/7.5 | Binary-Artifacts — no binaries found in the repo |
| 0/7.5 | Branch-Protection — branch protection not enabled on development/release branches |
| 0/2.5 | CI-Tests — keine Daten |
| 0/2.5 | CII-Best-Practices — no effort to earn an OpenSSF best practices badge detected |
| 0/7.5 | Code-Review — Found 0/30 approved changesets -- score normalized to 0 |
| 2.5/2.5 | Contributors — project has 35 contributing companies or organizations |
| 0/10 | Dangerous-Workflow — dangerous workflow patterns detected |
| 7.5/7.5 | Dependency-Update-Tool — update tool detected |
| 0/5 | Fuzzing — project is not fuzzed |
| 2.5/2.5 | Lizenz — license file detected |
| 0/7.5 | Maintained — 0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0 |
| 5/5 | Packaging — packaging workflow detected |
| 3.5/5 | Pinned-Dependencies — dependency not pinned by hash detected -- score normalized to 7 |
| 0/5 | SAST — no SAST tool detected |
| 0/5 | Security-Policy — security policy file not detected |
| 0/7.5 | Signed-Releases — keine Daten |
| 0/7.5 | Token-Permissions — detected GitHub workflow tokens with excessive permissions |
| 7.5/7.5 | Vulnerabilities — 0 existing vulnerabilities detected |
Verwendete Eingangsdaten
| source | openssf_scorecard |
| checks_evaluated | 16 |
| scorecard_version | v5.5.0 |
| checks_inconclusive | 2 |
| scorecard_aggregate | 3,8 |
Von der Bewertung ausgeschlossen (keine Daten oder nicht anwendbar): ci_tests, signed_releases. Die verbleibenden Gewichte wurden renormalisiert.
AI Readiness
Wie gut ist das Repository dafür ausgestattet, mit KI-Coding-Agenten entwickelt und gepflegt zu werden? Ein unabhängiges, experimentelles Badge — Gewicht 0,0, es wird eigenständig ausgewiesen und verändert den Gesamt-Gesundheitswert nicht.
51
AI-Agentenkontext & Leitlinien
40Gefährdet
Wie die Bewertung erfolgt
| 0/45 | Agentenanweisungen — keine CLAUDE.md / AGENTS.md / Editor-Regeln |
| 0/15 | Maschinenlesbare Doku (llms.txt) |
| 40/40 | Lesbare Commit-Historie — 97 von 97 menschlichen Commits benennen ihre Absicht (strukturierter Betreff oder erläuternder Text) |
Verwendete Eingangsdaten
| has_llms_txt | nein |
| legible_history_share | 1 |
| agent_instruction_files | — |
| agent_instruction_max_bytes | — |
Wie die Bewertung erfolgt
| 18/18 | Bootstrap mit einem Befehl — GNUmakefile |
| 22/22 | Automatisierte Tests |
| 0/11 | Lint-/Format-Konfiguration |
| 0/11 | Statische Typprüfung |
| 10/10 | Reproduzierbare Umgebung — devcontainer, Dockerfile |
| 0/10 | Belegte Agentenpraxis — keine von Agenten verfassten Commits unter den letzten 100 |
| 5/8 | Automatisierte Wartung — Abhängigkeits-Automatisierung konfiguriert, in den erfassten Commits nicht beobachtet |
| 7/10 | OpenSSF Scorecard: Pinned-Dependencies — dependency not pinned by hash detected -- score normalized to 7 |
Verwendete Eingangsdaten
| has_nix | nein |
| has_tests | ja |
| lockfiles | — |
| has_dockerfile | ja |
| typed_language | nein |
| bootstrap_files | GNUmakefile |
| has_devcontainer | ja |
| has_linter_config | nein |
| typecheck_configs | — |
| agent_commit_share | 0 |
| toolchain_manifests | — |
| dependency_bot_commit_share | 0 |
AI-Code-Lesbarkeit für Modelle
55Mittel
Wie die Bewertung erfolgt
| 0/45 | Typprüfbarer Code — Lean ohne Typprüfungs-Konfiguration |
| 55/55 | Handhabbare Dateigrößen — 0/12 Quelldateien über 60 KB |
Verwendete Eingangsdaten
| primary_language | Lean |
| largest_source_bytes | 24.562 |
| source_files_sampled | 12 |
| oversized_source_files | 0 |
Maschinenlesbare AI-Schnittstellen
40Gefährdet
Wie die Bewertung erfolgt
| 0/40 | API-Schema (OpenAPI/GraphQL/proto) |
| 0/20 | MCP-Server |
| 40/40 | Lauffähige Beispiele — examples |
Verwendete Eingangsdaten
| example_dirs | examples |
| has_mcp_signal | nein |
| api_schema_files | — |
Eckdaten
0GitHub-Sterne
99Mitwirkende
0Commits, letzte 12 Monate
129Tage seit letztem Push
14Releases
12Bus-Faktor
0offene Issues
—Paket-Ökosysteme
Warnungen zur Datenerhebung
- Community profile unavailable
- GitHub dependency-graph SBOM unavailable (404); the dependency graph may be disabled for this repository
Weitere Details
OpenSSF Scorecard 3.8 / 10
3.8Gesamtwert
Unabhängige, werkzeugneutrale Sicherheitsbewertung durch das quelloffene OpenSSF Scorecard. Jede Prüfung honoriert eine Sicherheits-Praxis, nicht das Werkzeug eines bestimmten Anbieters. Prüfungen, die Scorecard nicht ermitteln konnte, sind mit k. A. markiert und vom Sicherheitswert ausgeschlossen (nie als null gezählt).
| 10 | Binary-Artifacts | no binaries found in the repo |
| 0 | Branch-Protection | branch protection not enabled on development/release branches |
| k. A. | CI-Tests | no pull request found |
| 0 | CII-Best-Practices | no effort to earn an OpenSSF best practices badge detected |
| 0 | Code-Review | Found 0/30 approved changesets -- score normalized to 0 |
| 10 | Contributors | project has 35 contributing companies or organizations |
| 0 | Dangerous-Workflow | dangerous workflow patterns detected |
| 10 | Dependency-Update-Tool | update tool detected |
| 0 | Fuzzing | project is not fuzzed |
| 10 | License | license file detected |
| 0 | Maintained | 0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0 |
| 10 | Packaging | packaging workflow detected |
| 7 | Pinned-Dependencies | dependency not pinned by hash detected -- score normalized to 7 |
| 0 | SAST | no SAST tool detected |
| 0 | Security-Policy | security policy file not detected |
| k. A. | Signed-Releases | no releases found |
| 0 | Token-Permissions | detected GitHub workflow tokens with excessive permissions |
| 10 | Vulnerabilities | 0 existing vulnerabilities detected |
Alle Abhängigkeiten nicht erhoben
Der aufgelöste Abhängigkeitssatz konnte für diesen Bericht nicht erhoben werden: GitHub dependency-graph SBOM unavailable (404); the dependency graph may be disabled for this repository
JSON-Rohbericht maschinenlesbar
{
"data": {
"repo": {
"topics": [],
"is_fork": true,
"size_kb": 545579,
"has_wiki": true,
"homepage": "https://leanprover-community.github.io/mathlib4_docs",
"languages": {
"ASL": 2146,
"TeX": 13162,
"Lean": 77079927,
"Shell": 65934,
"Python": 93424,
"Makefile": 243,
"Dockerfile": 5669
},
"pushed_at": "2026-03-20T10:37:55Z",
"created_at": "2025-06-09T13:43:54Z",
"owner_type": "User",
"updated_at": "2025-12-10T16:05:22Z",
"description": "The math library of Lean 4",
"is_archived": false,
"is_disabled": false,
"license_spdx": "Apache-2.0",
"default_branch": "master",
"license_spdx_raw": "Apache-2.0",
"primary_language": "Lean",
"significant_languages": [
"Lean"
]
},
"owner": {
"blog": "mattrobball.com",
"name": "Matthew Robert Ballard",
"type": "User",
"login": "mattrobball",
"company": "@ICARM",
"location": "Columbia, South Carolina, USA",
"followers": 24,
"avatar_url": "https://avatars.githubusercontent.com/u/100034030?v=4",
"created_at": "2022-02-19T14:56:52Z",
"is_verified": null,
"public_repos": 37,
"account_age_days": 1619
},
"license": {
"state": "standard",
"spdx_id": "Apache-2.0",
"raw_spdx": "Apache-2.0",
"file_present": true,
"scorecard_found": true,
"profile_has_license": false
},
"activity": {
"releases": [
{
"tag": "v4.21.0-rc3",
"kind": "prerelease",
"published_at": "2025-06-04T13:46:02Z"
},
{
"tag": "v4.21.0-rc2",
"kind": "prerelease",
"published_at": "2025-06-04T06:26:00Z"
},
{
"tag": "v4.21.0-rc1",
"kind": "prerelease",
"published_at": "2025-06-03T08:51:00Z"
},
{
"tag": "v4.20.1",
"kind": "patch",
"published_at": "2025-06-04T13:56:59Z"
},
{
"tag": "v4.20.1-rc1",
"kind": "prerelease",
"published_at": "2025-06-04T07:43:25Z"
},
{
"tag": "v4.20.0",
"kind": "minor",
"published_at": "2025-06-02T15:58:18Z"
},
{
"tag": "v4.20.0-rc5",
"kind": "prerelease",
"published_at": "2025-05-09T10:19:47Z"
},
{
"tag": "v4.20.0-rc2",
"kind": "prerelease",
"published_at": "2025-05-05T07:39:49Z"
},
{
"tag": "v4.19.0",
"kind": "minor",
"published_at": "2025-05-01T17:26:36Z"
},
{
"tag": "v4.19.0-rc3",
"kind": "prerelease",
"published_at": "2025-04-13T11:28:09Z"
},
{
"tag": "v4.19.0-rc2",
"kind": "prerelease",
"published_at": "2025-04-03T08:58:06Z"
},
{
"tag": "v4.18.0",
"kind": "minor",
"published_at": "2025-04-01T05:56:39Z"
},
{
"tag": "v4.18.0-rc1",
"kind": "prerelease",
"published_at": "2025-03-03T14:53:41Z"
},
{
"tag": "v4.17.0",
"kind": "minor",
"published_at": "2025-03-03T13:06:30Z"
}
],
"recent_commits": [
{
"oid": "efe911a4cad7ab54c187dabca7f8ee633f099be9",
"body": "Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>",
"is_bot": false,
"headline": "chore(RingTheory/DedekindDomain): missing instances (#25613)",
"author_name": "Andrew Yang",
"author_login": "erdOne",
"committed_at": "2025-06-11T15:07:04Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "124c4b2dbc0734b284301706bdb17ebc3f3e924a",
"body": "…ro.map'` (#25660)\n\nfactored out of #22420\r\n\r\n\r\n\n\nCo-authored-by: Yaël Dillies <yael.dillies@gmail.com>",
"is_bot": false,
"headline": "feat(GroupWithZero/WithZero): injectivity and monotonicity of `WithZe…",
"author_name": "Yakov Pechersky",
"author_login": "pechersky",
"committed_at": "2025-06-11T14:29:58Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "4705244150fe57b4006d3393c5040d3d74e024b4",
"body": "Defines `FirstOrder.Language.Term.substFunc`, a way to substitute function definitions inside of a term. Compare this with existing `subst`, which just substitutes variables.\r\n\r\n\n\nCo-authored-by: Alex Meiburg <timeroot.alex@gmail.com>",
"is_bot": false,
"headline": "feat(ModelTheory/Syntax): substFunc (#23504)",
"author_name": "Alex Meiburg",
"author_login": "Timeroot",
"committed_at": "2025-06-11T13:32:22Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d7cd01678fb3d760f4e4f1f878b8b371364cf1fa",
"body": "Correct description of `finsum_mem_of_eqOn_zero` to say \"sum\" instead of \"product\"",
"is_bot": false,
"headline": "doc: typo fix (#25689)",
"author_name": "James Sundstrom",
"author_login": "js2357",
"committed_at": "2025-06-11T10:55:36Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "658f45e58d91b0fae574e3d6f6adf63ff72390ba",
"body": "Two lemmas for `realize`ing a `BoundedFormula`.\r\n\r\n\n\nCo-authored-by: Alex Meiburg <timeroot.alex@gmail.com>",
"is_bot": false,
"headline": "feat(ModelTheory/Semantics): BoundedFormula.realize_foldr_imp (#23502)",
"author_name": "Alex Meiburg",
"author_login": "Timeroot",
"committed_at": "2025-06-11T09:57:54Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "8024e6939a2a4f3e2d4546eaef31fac86ef16d14",
"body": "cf. [warning](https://github.com/leanprover-community/mathlib4/actions/runs/15570555569/job/43845188937#step:4:1) and [the action source](https://github.com/leanprover-community/lint-style-action/blob/6d296605703d65c27f1b4c5b19a92adcdec210ca/action.yml#L27)",
"is_bot": false,
"headline": "fix(bot_fix_style): use correct input name (#25678)",
"author_name": "Bryan Gin-ge Chen",
"author_login": "bryangingechen",
"committed_at": "2025-06-11T08:38:47Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "02c9f7384f5997119329584a4bc3137d60121ea9",
"body": null,
"is_bot": false,
"headline": "chore: silence more workflows on forks (#25685)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-11T07:05:57Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f650072af00e6e39a2980db19aeb8444f9a2d626",
"body": null,
"is_bot": false,
"headline": "fix: download oleans from main cache before fork cache (#25682)",
"author_name": "Kim Morrison",
"author_login": "kim-em",
"committed_at": "2025-06-11T06:34:29Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3b2e97bf3650b686d878f06720131571ed632690",
"body": "…_iff (#25673)\n\nThis PR fixes the statement of the lemma `boundaryLE_embeddingUpIntLE_iff`.",
"is_bot": false,
"headline": "chore(Algebra/Homology): fix ComplexShape.boundaryLE_embeddingUpIntLE…",
"author_name": "Joël Riou",
"author_login": "joelriou",
"committed_at": "2025-06-11T04:53:15Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "eb9a84806b2d0dea5ff10f006a4372d4e7649e5b",
"body": null,
"is_bot": false,
"headline": "chore: improve formatting of lists in documentation (#25655)",
"author_name": "Ruben Van de Velde",
"author_login": "Ruben-VandeVelde",
"committed_at": "2025-06-11T04:53:14Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "bd82942c8015d89bf91fd44c615680b65b4f48b6",
"body": "Deprecate the two `forall_in_swap` that are superseded by two applications of `forall_swap`, or `tauto`",
"is_bot": false,
"headline": "chore: deprecate `forall_in_swap` (#25670)",
"author_name": "Yaël Dillies",
"author_login": "YaelDillies",
"committed_at": "2025-06-11T04:10:38Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "98801bb29ee88222b06317c86e9b304ae52e2bba",
"body": "Given a category `J` (with `J : Type u` and `[Category.{v} J]`) and a functor `F : J ⥤ Type w`, we introduce a type `F.ColimitType : Type (max u w)`, which satisfies a certain universal property of the colimit: it is defined as a suitable quotient of `Σ j, F.obj j`. This universal property is not ex\n[…]\nheory.Limits.Types`, but we expand the API (with minimal imports to category theory) so that it may be used in future PRs to refactor both `DirectedSystem` and the construction of colimits in `Type`.)",
"is_bot": false,
"headline": "feat(CategoryTheory): the colimit type of a functor to types (#23339)",
"author_name": "Joël Riou",
"author_login": "joelriou",
"committed_at": "2025-06-11T01:58:48Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "380617b94b02699e3de24bf94f5b28a93495d5c5",
"body": "…orkflow (#25681)\n\nThis PR adds a comprehensive migration script to help mathlib4 contributors transition from direct write access to using a fork-based workflow. The script automates fork creation, remote setup, branch migration, and PR handling with intelligent detection of already-completed steps\n[…]\nnprover-community/mathlib4\r\n4. To update other branches, checkout and run this script again\r\n```\r\n\r\nI've exercised most of the logic, but this is AI written, so some further testing would be nice. :-)",
"is_bot": false,
"headline": "feat: add migrate_to_fork.py script for transitioning to fork-based w…",
"author_name": "Kim Morrison",
"author_login": "kim-em",
"committed_at": "2025-06-11T00:55:38Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "832b4eabd398b42dba1578b0445bd6070897a51d",
"body": "…iable declaration (#25677)\n\nNoticed while reviewing #25562. Prefer `{X : Type*}` over `{X}` as the latter introduces a universe metavariable.\r\nThese are the only occurrences of `X` in that file; #25562 will add two more.",
"is_bot": false,
"headline": "chore(Analysis/Normed/Operator/BoundedLinearMaps): centralise one var…",
"author_name": "grunweg",
"author_login": "grunweg",
"committed_at": "2025-06-11T00:55:37Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ae6b4f3cbfae6902dd3749aa13b76239d325aeb2",
"body": "This PR adds a new comprehensive user activity analysis script to help maintainers understand repository access patterns and user activity. The script analyzes all repository collaborators and organization members, shows last commit activity sorted by recency, displays access levels, includes intell\n[…]\nging and analysis. Documentation updated in scripts/README.md with detailed feature descriptions.\r\n\r\nGenerates tables like:\r\n```\r\nUsername Last Commit Access Level Profile",
"is_bot": false,
"headline": "feat: user activity report script (#25658)",
"author_name": "Kim Morrison",
"author_login": "kim-em",
"committed_at": "2025-06-11T00:20:11Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "17747760b00bd79a78cbfa326eb0fa3e8eedb475",
"body": "From Toric",
"is_bot": false,
"headline": "feat: if `p = a * b` is irreducible, then `a = 1` or `b = 1` (#24913)",
"author_name": "Yaël Dillies",
"author_login": "YaelDillies",
"committed_at": "2025-06-11T00:20:09Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9c94d13c156fef8a7f5f756ff75b2e0ddc91ecbe",
"body": "Pointed cones too are a kind of algebraic cone. They therefore move to the new `Geometry.Convex.Cone` folder.\r\n\r\nIn turn, this makes proper cones the primitive kind of topological/analytic cones, and therefore `Analysis.Convex.Cone.Proper` gets renamed to `Analysis.Convex.Cone.Basic`.\r\n\r\nThe two sec\n[…]\nne.InnerDual`.\r\n\r\nThe READMEs about `Geometry.Convex.Cone` and `Analysis.Convex.Cone` get updated to reflect that the separation is non-topology vs topology, rather topology vs analysis.\r\n\r\nFrom Toric",
"is_bot": false,
"headline": "chore: move pointed cones, proper cones (#25251)",
"author_name": "Yaël Dillies",
"author_login": "YaelDillies",
"committed_at": "2025-06-11T00:07:49Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "853aa9e9be1affcd90daad6d3a9e05fcb739885c",
"body": "Follow-up to #25558",
"is_bot": false,
"headline": "chore: deprecate RestrictedProduct file (#25679)",
"author_name": "Kevin Buzzard",
"author_login": "kbuzzard",
"committed_at": "2025-06-10T23:58:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0ca225f92121104c5ea959e234c049ecfd149fd1",
"body": "`Mathlib/Topology/Algebra/RestrictedProduct.lean` is over 1000 lines and we have over 500 lines more of restricted product API in FLT with more to come, so I thought I would split sooner rather than later.",
"is_bot": false,
"headline": "chore: split Mathlib/Topology/Algebra/RestrictedProduct (#25558)",
"author_name": "Kevin Buzzard",
"author_login": "kbuzzard",
"committed_at": "2025-06-10T22:59:05Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "4523c8f52c7d7c9851efd73187abf147ac7b9514",
"body": "This PR implements support for the `_ → _` relation in the `gcongr` tactic.\r\n\r\nThis can be useful in its own right, but the main reason for this is to later implement the `grw` and `gconvert` tactic using this infrastructure.\r\n\r\nTo be more specific, `_ → _` is now supported as a relation, *and* as a\n[…]\nnew goals to use `≤` instead of `<`.\r\n\r\n[#mathlib4 > Rewrite with inequalities @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Rewrite.20with.20inequalities/near/522751787)",
"is_bot": false,
"headline": "feat: let `gcongr` deal with implications (#25534)",
"author_name": "JovanGerb",
"author_login": "JovanGerb",
"committed_at": "2025-06-10T22:11:22Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "bbc23162e0b98efb0006003e78c4e914fe09e49f",
"body": null,
"is_bot": false,
"headline": "chore: fix spelling mistakes (#25674)",
"author_name": "euprunin",
"author_login": "euprunin",
"committed_at": "2025-06-10T21:12:37Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ad4fe0ea7ea151e70dfc1134111bb923c4a80d78",
"body": "…s (#25676)\n\nSnippet copied from `build_fork.yml`.",
"is_bot": false,
"headline": "chore: limit GITHUB_TOKEN permissions on pull_request_target workflow…",
"author_name": "Bryan Gin-ge Chen",
"author_login": "bryangingechen",
"committed_at": "2025-06-10T20:52:44Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "8b578dd922c8cbe52282cb2da4762611d16f5bc1",
"body": "…topological group, as an open normal subgroup (#25668)",
"is_bot": false,
"headline": "feat: add path component of the identity in a locally path connected …",
"author_name": "Jireh Loreaux",
"author_login": "j-loreaux",
"committed_at": "2025-06-10T20:04:58Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "45feb5a2692e7217df87d0a5e7efb1bb3b0cd881",
"body": "Apply the correct quotations to the json fields.",
"is_bot": false,
"headline": "fix(CI); autolabel correct json fields (#25661)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-10T14:59:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d6445160feb76acec3dbbcd3ce494b43efce415b",
"body": "```\r\ntheorem range_le_range_iff_ker_le_ker {U : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hU : U.IsSymmetric) :\r\n range T ≤ range U ↔ ker U ≤ ker T := by\r\n```\r\nand the forward direction holds in the infinite dimensional case too.\r\n\r\nUpstreamed from [quantumInfo](https://github.com/Timeroot/Lean-QuantumInfo)\r\n\r\n\n\nCo-authored-by: Alex Meiburg <timeroot.alex@gmail.com>",
"is_bot": false,
"headline": "feat(Analysis/InnerProductSpace): exchange range + ker (#25417)",
"author_name": "Alex Meiburg",
"author_login": "Timeroot",
"committed_at": "2025-06-10T14:32:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "fa2a544b28453a4179cc78f8c36f42c2b8b6f4e0",
"body": "The previous PR checked out code and placed HEAD on `master` rather than at the PR branch.",
"is_bot": false,
"headline": "fix(CI): autolabel compares branch with master (#25652)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-10T13:56:39Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5bc4d646aecec3da94984c7bd4b1fbdf71e47ce2",
"body": "…iff_orthogonal_le_orthogonal` and similars (#25240)",
"is_bot": false,
"headline": "feat(Analysis/InnerProductSpace/Projection): add lemma `Submodule.le_…",
"author_name": "Iván Renison",
"author_login": "IvanRenison",
"committed_at": "2025-06-10T13:25:42Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "53bf14c6d6d77793ed9553cb24ffd119f9751cc9",
"body": "We no longer rely on `autolabel` to add the label via `gh`, but use a commandline `curl` instead.",
"is_bot": false,
"headline": "fix(C): autolabel applies the label using curl (#25641)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-10T13:13:20Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f61f9e0e4861327e87d4719ea52f78db7112d914",
"body": "Update two links in the docstring which weren't updated when files moved to a subfolder.",
"is_bot": false,
"headline": "doc(MeasureTheory/Integral/Bochner): update links in docstring (#25647)",
"author_name": "Oliver Butterley",
"author_login": "oliver-butterley",
"committed_at": "2025-06-10T12:33:46Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "2066888d5aa71c573080c0e58c06f41db98c9bc7",
"body": "…iff its closure has finite index (#23312)\n\nLet `u : Fin (rank K) → (𝓞 K)ˣ` be a family of units of a number field `K`. We prove that `isMaxRank u`, that is its regulator is nonzero, iff `closure (Set.range u))` has finite index.",
"is_bot": false,
"headline": "feat(NumberField/Units): prove that a family of units is of max rank …",
"author_name": "Xavier Roblot",
"author_login": "xroblot",
"committed_at": "2025-06-10T11:18:57Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b19461d86110b60c74051d57bbaf1efc1768d067",
"body": "Use the new definition `analyticOrderAt` to provide a version of `AnalyticOnNhd.codiscrete_setOf_analyticOrderAt_eq_zero_or_top` that is easier to use, since it avoids hassle with subtypes and subsets. Provide easy-to-use special cases about the discreteness of the zero locus of analytic functions.",
"is_bot": false,
"headline": "feat: improve API for isolated zeros of analytic functions (#25643)",
"author_name": "Stefan Kebekus",
"author_login": "kebekus",
"committed_at": "2025-06-10T11:05:59Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "39d8416ae1e1083477f7546f1fd10e460ad37936",
"body": "Given a quiver with decidable equality on its vertices and arrows, we construct an instance of decidable equality for `Quiver.Path`. We proceed through a recursion on the length of the path utilizing an intermediate subtype of uniformly bounded paths `Quiver.Path.BoundedPath`.\n\nThis was motivated by doing computations on small quivers with Lean.\n\n\n\nCo-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>",
"is_bot": false,
"headline": "feat: decidable equality for `Quiver.Path` (#25623)",
"author_name": "Matthew Robert Ballard",
"author_login": "mattrobball",
"committed_at": "2025-06-10T10:01:48Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5db2d4df25746b0b19b588e0d6be79ed4da95278",
"body": "… (#22834)\n\nGiven a parametrized adjunction `adj₂ : F ⊣₂ G` between bifunctors `F : C₁ ⥤ C₂ ⥤ C₃` and `G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂`, three maps `f₁ : X₁ ⟶ Y₁` in `C₁`, `f₂ : X₂ ⟶ Y₂` in `C₂`, and `f₃ : X₃ ⟶ Y₃` in `C₃`, this PR shows that `f₃` has the right lifting property with respect to the \"inclusion\" of\n[…]\nelia Livingston <101damnations@github.com>\nCo-authored-by: JovanGerb <jovan.gerbscheid@gmail.com>\nCo-authored-by: Jireh Loreaux <loreaujy@gmail.com>\nCo-authored-by: Oliver Nash <github@olivernash.org>",
"is_bot": false,
"headline": "feat(CategoryTheory): lifting properties and parametrized adjunctions…",
"author_name": "Joël Riou",
"author_login": "plp127",
"committed_at": "2025-06-10T09:42:12Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "855ce5ce821cc42e2147ea69c03c212c672bca3b",
"body": null,
"is_bot": false,
"headline": "ci: reporting success should include post build checks (#25642)",
"author_name": "Johan Commelin",
"author_login": "jcommelin",
"committed_at": "2025-06-10T08:10:57Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7c2e3ba444cfc1c16f84eaec71e75b70e1e1839b",
"body": null,
"is_bot": false,
"headline": "feat: add AlgHom.natCard_of_splits (#25253)",
"author_name": "Ruben Van de Velde",
"author_login": "Ruben-VandeVelde",
"committed_at": "2025-06-10T07:34:29Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0e832cb41d406dc3c36bccead1fb0f1015f53ca7",
"body": "This lemma loops with `IsMon_Hom.one_hom` applied to `(λ_ N.X).inv`, as evidenced by the following trace:\r\n```\r\n[Meta.Tactic.simp.rewrite] Mon_Class.tensorObj.one_def:1000:\r\n Mon_Class.one\r\n ==>\r\n (λ_ (𝟙_ C)).inv ≫ (Mon_Class.one ⊗ Mon_Class.one)\r\n[Meta.Tactic.simp.rewrite] id_tensorHom\n[…]\n the equivalent of `map_one` while `one_def` is not fine since it is the equivalent of `Algebra.TensorProduct.one_def`.\r\n\r\nDo the same thing for the `mul` lemmas and the `Mon_` versions.\r\n\r\nFrom Toric",
"is_bot": false,
"headline": "chore(CategoryTheory): unsimp `Mon_Class.tensorObj.one_def` (#25601)",
"author_name": "Yaël Dillies",
"author_login": "YaelDillies",
"committed_at": "2025-06-10T06:49:57Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "fe12b92d4f441acfac152e00848988e774befe5c",
"body": "We define a class `HasFibers p` for a given functor `p : 𝒳 ⥤ 𝒮`. The point of this is to give the user the option to supply their own fiber categories, as often the standard fibers will not be definitionally the same as the (equivalent) categories one is interested in.\r\n\r\nCo-authored-by: Paul Lezeau <paul.lezeau@gmail.com>",
"is_bot": false,
"headline": "feat(FiberedCategory/HasFibers): define HasFibers class (#13611)",
"author_name": "Calle Sönne",
"author_login": "callesonne",
"committed_at": "2025-06-10T06:43:25Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "05be7e6bf7366c9e3d233917e5fdb0ce5f127b1c",
"body": "This PR removes the `Lean.githash` component of `cache`s hashing function.\r\n\r\nThis enables running `cache` compiled on one toolchain against a checkout on another toolchain.\r\n\r\nHowever, this (as advertised in the deleted comment) will break CI for the `lean-pr-testing-NNNN` toolchains. This is not a\n[…]\nthese is presumed broken anyway as a result of recent CI upgrades. We will fix this shortly by tagging the `lean-pr-testing-NNNN` toolchains with an embedded hash, e.g. `lean-pr-testing-1234-ab57ce3`.",
"is_bot": false,
"headline": "feat: don't use `Lean.githash` in `cache` hashing (#25639)",
"author_name": "Kim Morrison",
"author_login": "kim-em",
"committed_at": "2025-06-10T05:54:11Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "30b4d6e87eaaa93450a25e8ad795bf3596275589",
"body": "Discovered while investigating why the bot has been failing recently: this will likely not fix the bot, but should be updated anyway!",
"is_bot": false,
"headline": "chore: use non-deprecated function in bench_summary (#25495)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-09T23:58:24Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3e523a149fa63dde0651c6b3272c1737b37edc6c",
"body": "…nneg_eigenvalues` (#25493)",
"is_bot": false,
"headline": "feat(Analysis/InnerProductSpace/Positive): add theorem `IsPositive.no…",
"author_name": "Iván Renison",
"author_login": "IvanRenison",
"committed_at": "2025-06-09T23:51:33Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ea33796baf279603f94007e934e2245c4a0d27a4",
"body": null,
"is_bot": false,
"headline": "fix: add missing simps projections for ContinuousAddEquiv (#24892)",
"author_name": "Ruben Van de Velde",
"author_login": "Ruben-VandeVelde",
"committed_at": "2025-06-09T23:04:40Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "4bc3282320af58a0d05d3d2e5076b8926bfe4457",
"body": "This PR updates the Mathlib dependencies.",
"is_bot": true,
"headline": "chore: update Mathlib dependencies 2025-06-09 (#25627)",
"author_name": "mathlib4-update-dependencies-bot",
"author_login": "mathlib-bors[bot]",
"committed_at": "2025-06-09T20:54:46Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7b3a5561f0803e0f4d5f38ab0df6bd6f0a288fff",
"body": "Continuation from #18621.\r\n\r\nFrom the ExponentialRamsey project.",
"is_bot": false,
"headline": "feat(SpecialFunctions/Log): more continuity and limits for logb (#18912)",
"author_name": "Bhavik Mehta",
"author_login": "b-mehta",
"committed_at": "2025-06-09T18:47:13Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e99fde22b3578f46d1e7cdced350239463c1d914",
"body": "If `master` is on a different toolchain than the PR, then its `mk_all` doesn't work; we fix that by just running the PR branch's version of `mk_all` inside `landrun`.",
"is_bot": false,
"headline": "fix: run pr branch version of mk_all (#25624)",
"author_name": "Bryan Gin-ge Chen",
"author_login": "bryangingechen",
"committed_at": "2025-06-09T17:35:50Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3c689580a42d979448dfe65b37ce9e858d993f8f",
"body": "Removes extraneous lemmas from `Ring/Hom/Basic`.\r\n\r\n\n\nCo-authored-by: Wrenna Robson <wren.robson@gmail.com>",
"is_bot": false,
"headline": "fix: Remove lemmas from `Ring/Hom/Basic` (#25447)",
"author_name": "Wrenna Robson",
"author_login": "wrenna-robson",
"committed_at": "2025-06-09T16:45:50Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f8584e63b902a6965d4eddbe2ff6f3b3003381c3",
"body": "Fill in simple lemmas as convenient special cases with the right syntactic equalities for rewrites.",
"is_bot": false,
"headline": "feat(Finset/SymmDiff): add additional api lemmas (#25553)",
"author_name": "Bhavik Mehta",
"author_login": "b-mehta",
"committed_at": "2025-06-09T16:08:09Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "4141bd5ee664edd57dccd75a2b72caecbb922839",
"body": "… is equivalent with dirac measure evaluation (#25396)\n\nMathlib has `mem_ae_dirac_iff` that provides `s ∈ ae (dirac a) ↔ a ∈ s`, which expands to `(dirac a) sᶜ = 0 ↔ a ∈ s`. A more natural statement (arguably) is `(dirac a) s = 1 ↔ a ∈ s`.\r\n\r\nThis feature adds `(dirac a) s = 1 ↔ a ∈ s` and a compani\n[…]\ns merged.\r\n\r\n(Note, the proofs depend on `dirac` being a `ProbabilityMeasure`, hence why the theorems are where they are in Dirac.lean.)\r\n\r\n\n\nCo-authored-by: bwehlin <bwehlin@users.noreply.github.com>",
"is_bot": false,
"headline": "feat (MeasureTheory/Measure/Dirac): a point being in a measurable set…",
"author_name": "bwehlin",
"author_login": "bwehlin",
"committed_at": "2025-06-09T15:56:27Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "d24f7121ba1ee50e9df804c212133604660a9436",
"body": "…fferential (#25589)\n\nCo-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>",
"is_bot": false,
"headline": "feat(RingTheory/DedekindDomain): unramified primes does not divide di…",
"author_name": "Andrew Yang",
"author_login": "erdOne",
"committed_at": "2025-06-09T15:24:34Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d9ad6f7f5c6f83c18419a1cab4d95f8fc1462a38",
"body": "…hapes.AbelianImages): minimize hypotheses (#25185)\n\nMinimize the hypotheses needed for the definition of `Abelian.image`, `Abelian.Coimage` and the definitions associated to them, as well as for `PreservesImage.iso` and `PreservesCoimage.iso` (the isomorphisms expressing that a functor commutes wit\n[…]\nHasKernels`/`HasCokernels` instances by instances involving only the precise kernels/cokernels that are needed.\r\n(This is useful for one of my projects, where I don't yet know that all kernels exist.)",
"is_bot": false,
"headline": "feat(CategoryTheory.Abelian.Images, CategoryTheory.Limits.Preserves.S…",
"author_name": "smorel394",
"author_login": null,
"committed_at": "2025-06-09T15:16:38Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "51f395a11e621d783e280335ceb1a5c6c6248014",
"body": "… (#25443)\n\nI am going to be adding some more summability results for Eisenstein series (for example for E2), so it makes sence for this to all be in a separate file.",
"is_bot": false,
"headline": "chore : Split summability results for Eisenstein series into own file…",
"author_name": "Chris Birkbeck",
"author_login": "CBirkbeck",
"committed_at": "2025-06-09T13:00:04Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c9a191be40d6f147aa466f25016fdcd251242aab",
"body": "…NNReal`-linear functionals (#24265)\n\nprove the Riesz-Markov-Kakutani theorem for `NNReal`-linear functional, by reducing the statement to the `Real`-version, but for `lintegral` instead of `integral`.\r\n\r\nThe bulk of the PR is the definitions and lemmas to go back and forth between `Real` and `NNReal` linear functionals.\r\n\r\nMotivation: this is the version first aimed at, perhaps for applications in probability.\n\nCo-authored-by: Yoh Tanimoto <hoyt@jcom.home.ne.jp>",
"is_bot": false,
"headline": "feat(MeasureTheory/Integral): the Riesz-Markov-Kakutani theorem for `…",
"author_name": "Yoh Tanimoto",
"author_login": "yoh-tanimoto",
"committed_at": "2025-06-09T12:09:13Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "eb04d3dfad4e7f811d3fd6c85d552dfd5a8274ba",
"body": "…25413)\n\nThis fixes the instances diamonds in the `Rat` and `NNRat` actions, and adds lemmas about `{Nat,Int,NNRat,NRat}.cast`and `of{Nat,Scientific}`.\r\n\r\nThere is no motivation here beyond cleaning up diamonds.",
"is_bot": false,
"headline": "fix(HahnSeries): solve `SMul Rat` diamonds, and lemmas about casts (#…",
"author_name": "Eric Wieser",
"author_login": "eric-wieser",
"committed_at": "2025-06-09T11:40:12Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d8fba24f987c655793fe3d1294e4fd2d68925d82",
"body": "This PR updates the Mathlib dependencies.",
"is_bot": true,
"headline": "chore: update Mathlib dependencies 2025-06-09 (#25618)",
"author_name": "mathlib4-update-dependencies-bot",
"author_login": "mathlib-bors[bot]",
"committed_at": "2025-06-09T10:59:15Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "210d1c312c648203a35b599192b20e1013e5116f",
"body": "for `OneHom.mulSingle` and `MonoidHom.mulSingle`.",
"is_bot": false,
"headline": "feat(Algebra/Group/Pi): add injectivity and coe lemmas (#25525)",
"author_name": "Peiran Wu",
"author_login": "wupr",
"committed_at": "2025-06-09T10:18:17Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "fe653fb930c0c9c876267b109287322a055e12a0",
"body": null,
"is_bot": false,
"headline": "feat(Data/Fin): `Fin.castLE` on the result of a cast from `Nat` (#25083)",
"author_name": "Jakob von Raumer",
"author_login": "javra",
"committed_at": "2025-06-09T09:08:14Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "64678d94d57d7470ed8e72c981e32558f043033e",
"body": "If `μ` is gaussian, then `μ.map (fun x ↦ x + c)` is gaussian as well.\r\nThe same is true for `c + x`, `x - c`, `-x` and `c - x` instead of `x + c`.",
"is_bot": false,
"headline": "feat(Probability): translations of gaussians are gaussian (#25532)",
"author_name": "Rémy Degenne",
"author_login": "RemyDegenne",
"committed_at": "2025-06-09T09:00:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b2a691d28e92758e26984b1db78d9e6539a86d06",
"body": "The third of 3 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, this is the projective resolution of `k` as a trivial `G`-representation whose `n`th object is \r\n`Gⁿ →₀ k[G]` with representation defined pointwise by the left regular representation on \n[…]\nc. We carry the exactness properties across this isomorphism to conclude the bar resolution is a projective resolution too, in `Rep.barResolution`.\r\n\r\n\n\nCo-authored-by: 101damnations <al3717@ic.ac.uk>",
"is_bot": false,
"headline": "feat(RepresentationTheory/*): add the bar resolution (#21738)",
"author_name": "Amelia Livingston",
"author_login": null,
"committed_at": "2025-06-09T08:15:24Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "7deb334c5f5104f4edad1a6396dd02a8cddefb86",
"body": null,
"is_bot": false,
"headline": "chore: deprime `induction` in `GroupTheory` (#25353)",
"author_name": "Jeremy Tan Jie Rui",
"author_login": "Parcly-Taxel",
"committed_at": "2025-06-09T05:02:15Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9168cb3c598586220481137e6e99332eea930727",
"body": "Factored out from #22420",
"is_bot": false,
"headline": "feat(GroupWithZero): monoid with zero homs to (co)products (#25466)",
"author_name": "Yakov Pechersky",
"author_login": "pechersky",
"committed_at": "2025-06-09T04:25:39Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "18fc2693a603f23ffda0e45a2983ccf374aa1323",
"body": "Currently bors requires status checks named \"Build\" and \"Lint Style\" to succeed before it will merge a PR; however, for PRs from forks, the status checks are named \"Build (fork)\" and \"Lint Style (fork)\". To solve this, we create a no-op job downstream from the two jobs with the name \"CI Success\" and\n[…]\nmit, as opposed to a job in a workflow triggered by `pull_request_target` or `push` etc. In principle we could have done some stuff with the GitHub API to fix this, but the approach here seems easier.",
"is_bot": false,
"headline": "chore: let bors merge PRs from forks (#25614)",
"author_name": "Bryan Gin-ge Chen",
"author_login": "bryangingechen",
"committed_at": "2025-06-09T04:10:34Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "02aed454ae7880b5ade42e22bb929144df53f386",
"body": "Currently, the \"Style Lint (fork)\" job is triggered even for PRs from branches in this repo. We add the fork conditional to all jobs in order to fix this.",
"is_bot": false,
"headline": "fix: only run jobs in the fork workflow for PRs from forks (#25615)",
"author_name": "Bryan Gin-ge Chen",
"author_login": "bryangingechen",
"committed_at": "2025-06-09T03:42:04Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "fb2feae156bb82f905351998a7a5a4db17ce7b04",
"body": "This PR updates the Mathlib dependencies.",
"is_bot": true,
"headline": "chore: update Mathlib dependencies 2025-06-09 (#25610)",
"author_name": "mathlib4-update-dependencies-bot",
"author_login": "mathlib-bors[bot]",
"committed_at": "2025-06-09T02:22:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "8b8fe2fa631658e55895b284747a997a249d3599",
"body": null,
"is_bot": false,
"headline": "fix(CI): prevent another emoji reaction from forks (#25598)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-08T18:48:14Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "1150bf562665cebc5bbf10fdf12f5a293a703f56",
"body": "…r` (#24257)\n\nThis PR generalizes `PFunctor` to have potentially different universe levels for its `A` and `B` fields. This is to aid with my formalization attempt (with @dtumad ) of poly functors [here](https://github.com/dtumad/VCV-io/blob/master/ToMathlib/PFunctor/Basic.lean) (in order to model interactive systems in general, and cryptographic protocols in particular).\r\n\r\nThere is no plan yet to need `MvPFunctor`, so I do not generalize universe levels of that for now.",
"is_bot": false,
"headline": "feat(Data/PFunctor/Univariate): Generalize universe level in `PFuncto…",
"author_name": "Quang Dao",
"author_login": "quangvdao",
"committed_at": "2025-06-08T17:42:39Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e1cc5c558996c408490de4cff6dc428c3b7eadbb",
"body": "This is a CI action that only runs on commits to master, which is why I had missed it earlier.",
"is_bot": false,
"headline": "fix(CI): yet another action that should not run from forks (#25594)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-08T16:31:22Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a4ec7db3014165e418ef1f634cfd5afbed2ce04f",
"body": "…r` (#25569)\n\nWe add `Functor.toPseudofunctor` which takes a functor between categories and returns the corresponding pseudofunctor between locally discrete categories. Previously, `Functor.toPseudofunctor` took a functor from a category to a _strict_ bicategory, and returned the corresponding pseudofunctor. Since this new construction works for all functors, I suggest that this takes the name `Functor.toPseudofunctor` and the latter gets renamed to `Functor.toPseudofunctor'`.",
"is_bot": false,
"headline": "feat(Bicategory/Functor/LocallyDiscrete): add `Functor.toPseudofuncto…",
"author_name": "Calle Sönne",
"author_login": "callesonne",
"committed_at": "2025-06-08T16:23:17Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d1c754c26e7bb83ba1f88f9a51e3c536722c769f",
"body": "…leGraph` (#22085)",
"is_bot": false,
"headline": "feat(Combinatorics/SimpleGraph): introduce `ConnectedComponent.toSimp…",
"author_name": "Iván Renison",
"author_login": "IvanRenison",
"committed_at": "2025-06-08T14:55:42Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b84acde320e524a278d2f3f18816bb93d71d4fc0",
"body": "These are the remaining actions using a non-`secrets.GITHUB_TOKEN` token. Hopefully this covers most, if not all, the reamining regular failures for actions on forks.\r\n\r\nThe previous PR with a similar effect was #25590.",
"is_bot": false,
"headline": "fix(CI): avoid running more mathlib4 only actions in forks (#25592)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-08T14:49:54Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "80b79be68fca5e62b2b224170595514b336b9e07",
"body": "Add some congr lemmas and a locally finset range lemma.",
"is_bot": false,
"headline": "feat(Topology/Algebra/InfiniteSum/UniformOn): add congr lemmas (#25446)",
"author_name": "Chris Birkbeck",
"author_login": "CBirkbeck",
"committed_at": "2025-06-08T14:36:36Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "32a7b4c048bda800ae6e17cc5984446ba1fff28e",
"body": "These are a few of the actions that report failures.",
"is_bot": false,
"headline": "fix(CI): avoid running mathlib4 only actions in forks (#25590)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-08T14:09:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9dbb163e576423ee953f0ee6f759f63714339162",
"body": "…#25367)\n\nThis is required to prove that A_n is simple iff n = 3 or 5 ≤ n: #23555",
"is_bot": false,
"headline": "feat: `Subgroup ↥(H : Subgroup G) ≃o { H' : Subgroup G // H' ≤ H }` (…",
"author_name": "Miyahara Kō",
"author_login": "Komyyy",
"committed_at": "2025-06-08T14:09:48Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "284e9184e3c66df8c1ab46e85f2cbf4e6b6c3e68",
"body": "…lity (#25576)\n\nAdd three simple lemmas and golf a fourth.",
"is_bot": false,
"headline": "feat(SetTheory/Cardinal): relate nonemptiness of a set to its cardina…",
"author_name": "Bhavik Mehta",
"author_login": "b-mehta",
"committed_at": "2025-06-08T11:29:55Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "563fcef08d127fadf331f555a12c1ea8c1f6d53f",
"body": "The docstring for `Matrix.toLin'` references `Matrix.vecMulLin`, which does not exist. This PR changes the docstring to correctly reference `Matrix.mulVecLin` instead.",
"is_bot": false,
"headline": "docs(LinearAlgebra/Matrix/ToLin): fix docstring (#25571)",
"author_name": "plp127",
"author_login": "plp127",
"committed_at": "2025-06-08T11:11:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0830de5843a83128a28a8ec3aa90ec9c572d61c9",
"body": "…#25581)\n\nLimit the `Dependent issues` actions to `leanprover-community/mathlib4`.",
"is_bot": false,
"headline": "fix(CI): run dependent issues only on leanprover-community/mathlib4 (…",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-08T10:58:09Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3bb3ee2af45a24bd1533f8e1803c06a5035a7070",
"body": "Replace `measurability` by `fun_prop` where it made a visible difference in elaboration time.",
"is_bot": false,
"headline": "perf: replace `measurability` by `fun_prop` (#25577)",
"author_name": "plp127",
"author_login": "plp127",
"committed_at": "2025-06-08T08:19:52Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c38c7fde32656c7fa1b2471ed1ae0d50a600f089",
"body": "Another PR trying to fix the PR summary from forks.\r\n\r\nWithout this change, the [error](https://github.com/leanprover-community/mathlib4/actions/runs/15494880040/job/43629089332?pr=25540) was `error: pathspec 'adomani/fork_test' did not match any file(s) known to git`.",
"is_bot": false,
"headline": "fix(PR summary): use hash instead of branch name (#25544)",
"author_name": "damiano",
"author_login": "adomani",
"committed_at": "2025-06-08T05:56:44Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "bb076f5f2d39b534b917755b0338314b6714304b",
"body": "…angle_add_angle_eq_pi` (#25559)\n\nIt turns out that `angle_add_angle_add_angle_eq_pi` can be proved with one condition less :)",
"is_bot": false,
"headline": "feat(Geometry/Euclidean/Triangle): remove hypothesis from `angle_add_…",
"author_name": "JovanGerb",
"author_login": "JovanGerb",
"committed_at": "2025-06-07T22:05:57Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f4848f31e6409cadd5955625c2cf7bef8d6c026d",
"body": "This PR fixes the naming and statement of transitivity lemmas for `≤` and `<`.\r\n\r\nIt deprecates `gt_of_ge_of_gt` and `gt_of_gt_of_ge`\r\n\r\nThe main changes are in `Mathlib.Order.Basic` and `Mathlib.Order.Defs.PartialOrder`",
"is_bot": false,
"headline": "chore(Order): use new ge/gt naming convention - Part 4 (#25572)",
"author_name": "JovanGerb",
"author_login": "JovanGerb",
"committed_at": "2025-06-07T20:52:57Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "6f872f1d3300e5877cb0874ea47000ab0911f04f",
"body": "Using this we can do things like:\r\n```lean\r\nattribute [simp] Matrix.one_fin_two\r\n#check !![2, -3; -1, 2].toPerfectPairing ⟨!![2, 3; 1, 2], by simp, by simp⟩ -- Works\r\n```",
"is_bot": false,
"headline": "feat: an invertible matrix as a perfect pairing (#25477)",
"author_name": "Oliver Nash",
"author_login": "ocfnash",
"committed_at": "2025-06-07T19:11:47Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "006201f19d874255716a8a2365a2a630984b1dc9",
"body": "This PR renames 4 more lemmas in Order.Basic.",
"is_bot": false,
"headline": "chore(Order): use new ge/gt naming convention - Part 3 (#25566)",
"author_name": "JovanGerb",
"author_login": "JovanGerb",
"committed_at": "2025-06-07T18:15:56Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f886ece749d2584376532f07d8ea74fc19f36d44",
"body": "This PR moves some lemmas in Order.Basic to the correct place.\r\n\r\nSome of the lemmas now only assume `LE` or `LT` instead of `Preorder`.\r\n\r\nFor example `le_of_le_of_eq` and `le_of_le_of_eq'` now have the same hypothesis.",
"is_bot": false,
"headline": "chore(Order/Basic): move lemmas to the correct section (#25568)",
"author_name": "JovanGerb",
"author_login": "JovanGerb",
"committed_at": "2025-06-07T17:32:35Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b2b0027d45dc08b0e365357a1a8013d6ca586304",
"body": null,
"is_bot": false,
"headline": "chore(Order): deprecate `gt_irrefl` (#25567)",
"author_name": "JovanGerb",
"author_login": "JovanGerb",
"committed_at": "2025-06-07T17:32:34Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "cb99f5a52ecf7a1ca248bef8c42ade620024df9a",
"body": "I have decided that depriming one folder (or part of a folder) at a time is the way to go.",
"is_bot": false,
"headline": "chore: deprime `induction` in `Archive` and `SetTheory` (#25512)",
"author_name": "Jeremy Tan Jie Rui",
"author_login": "Parcly-Taxel",
"committed_at": "2025-06-07T16:11:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "6c6e0180f0d3dc9f47f85532f48d268d8656789a",
"body": "This PR renames \r\nLT.lt.not_le -> LT.lt.not_ge\r\nLE.le.not_lt -> LE.le.not_gt\r\nLT.lt.not_lt -> LT.lt.not_gt",
"is_bot": false,
"headline": "chore(Order): use new ge/gt naming convention - Part 2 (#25560)",
"author_name": "JovanGerb",
"author_login": "JovanGerb",
"committed_at": "2025-06-07T15:55:08Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "6384b32ef57bec498faba845795a8e20e5cb9776",
"body": null,
"is_bot": false,
"headline": "feat: the Gamma function is meromorphic (#25538)",
"author_name": "Miyahara Kō",
"author_login": "Komyyy",
"committed_at": "2025-06-07T15:38:51Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c9603c6e6bf74d4a5b31da8aaaa69704dc0bf662",
"body": "Each of these lemmas has been upstreamed to core, and the deprecations are in favour of exactly identical statements.\r\n\r\nRenames:\r\n- `Nat.mul_right_eq_self_iff` -> `Nat.mul_eq_left`\r\n- `Nat.mul_left_eq_self_iff` -> `Nat.mul_eq_right`\r\n- `Nat.eq_zero_of_double_le` -> `Nat.eq_zero_of_two_mul_le`\r\n- `N\n[…]\nat.div_le_of_le_mul`\r\n- `Nat.div_le_self'` -> `Nat.div_le_self`\r\n\r\nBest reviewed commit-by-commit.\r\n\r\n[](https://gitpod.io/from-referrer/)",
"is_bot": false,
"headline": "chore(Nat): deprecate lemmas which are now in core (#25494)",
"author_name": "Bhavik Mehta",
"author_login": "b-mehta",
"committed_at": "2025-06-07T14:10:35Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "dcd738d0b6bab40bc1ab68d39472e77cbedf9219",
"body": "The main lemma is `t35Space_iff_isEmbedding_stoneCechUnit`.\r\nThis property is stated in [Wikipedia](https://en.wikipedia.org/wiki/Stone–Čech_compactification#Universal_property_and_functoriality).",
"is_bot": false,
"headline": "feat: tychonoff space ↔ embedded on Stone-Čech compactification (#24909)",
"author_name": "Miyahara Kō",
"author_login": "Komyyy",
"committed_at": "2025-06-07T14:03:54Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3433dea2c282523c59a6fb398f9250c40714f34c",
"body": "Add three `iff` lemmas which are often useful to compare cardinalities.",
"is_bot": false,
"headline": "feat(Finset/Card): relate cardinality of `s \\ t` with `t \\ s` (#25554)",
"author_name": "Bhavik Mehta",
"author_login": "b-mehta",
"committed_at": "2025-06-07T13:26:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "bf1171271afab2055ee6dd577146d47ccfc087f9",
"body": "…red additive monoids (#23888)",
"is_bot": false,
"headline": "feat: properties of graded rings indexed by canonically linearly orde…",
"author_name": "Jireh Loreaux",
"author_login": "j-loreaux",
"committed_at": "2025-06-07T12:40:59Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b5368c7d48612974c32bab5cebc280f2517b33be",
"body": "... by populating the `nsmul` and `zsmul` fields using the existing `SMul` instances (which must be moved earlier).\r\n\r\nThis also improves the defeq of `sub`.",
"is_bot": false,
"headline": "fix(HahnSeries): solve `SMul` diamonds (#25408)",
"author_name": "Eric Wieser",
"author_login": "eric-wieser",
"committed_at": "2025-06-07T11:09:34Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "bddb146ad166d576305d50841d8d0899052aeb77",
"body": "…#24982)\n\nThe bijection `mateEquiv` is essentially redefined as a composition of two bijections. The proofs are a little bit simpler as the constructions of each of these two bijections is an easier task. This also allows to prove a lemma `mateEquiv_eq_iff` which shall be used in the construction of the 2-category of adjunctions in a bicategory #13539.",
"is_bot": false,
"headline": "refactor(CategoryTheory/Bicategory/Adjunction): definition of mates (…",
"author_name": "Joël Riou",
"author_login": "joelriou",
"committed_at": "2025-06-07T10:03:42Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "827b149f0da56b6db07f406f48f9243693a0529d",
"body": "This is the first PR in a sequence of PRs to apply the new naming convention for order lemmas.\r\n\r\nThis PR changes some lemmas that have multiple occurences of `lt` or `le` in their name, and where `<` and `≤` have their arguments swapped in some places. Then those occurrences of `<` and `≤` are refe\n[…]\nriends, \r\n\r\nThe first commit is an automatic replacement of lemma names. The second commit adds deprecations for the renamed lemmas. Later commits are manual fixes. This should make it easy to review.",
"is_bot": false,
"headline": "chore(Order): use new `ge`/`gt` naming convention - Part 1 (#24775)",
"author_name": "JovanGerb",
"author_login": "JovanGerb",
"committed_at": "2025-06-07T10:03:41Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "e9d22cd4be1e303da73aa8c853602cd8e2334651",
"body": "…25546)\n\nThe second of 3 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, this is the projective resolution of `k` as a trivial `G`-representation whose `n`th object is \r\n`Gⁿ →₀ k[G]` with representation defined pointwise by the left regular represen\n[…]\nrties across this isomorphism to conclude the bar resolution is a projective resolution too, in `Rep.barResolution`.\r\n\r\nIn this PR we factor out some material from #21738, to make it easier to review.",
"is_bot": false,
"headline": "feat(RepresentationTheory/*): prerequisites for the bar resolution (#…",
"author_name": "Amelia Livingston",
"author_login": null,
"committed_at": "2025-06-07T09:38:08Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "bd7f0d6243fa265cd3251a5046111248e07ed421",
"body": "This also renames `SummableFamily.single` to `SummableFamily.const` (matching `Function.const`) to make room for `SummableFamily.single` (matching `Pi.single`).\r\n\r\nMoves:\r\n- `SummableFamily.single` -> `SummableFamily.const`",
"is_bot": false,
"headline": "feat(HahnSeries): `single_inv` and `single_div_single` (#25414)",
"author_name": "Eric Wieser",
"author_login": "eric-wieser",
"committed_at": "2025-06-07T08:13:22Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "8ee00f5b77b5fe306cc575caaf7e0b699ac0ee45",
"body": "…tionIdx`. (#25498)",
"is_bot": false,
"headline": "feat: connection between `Algebra.IsUnramifiedAt` and `Ideal.ramifica…",
"author_name": "Andrew Yang",
"author_login": "erdOne",
"committed_at": "2025-06-07T07:26:46Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a8c0ebf803b8e5745a6319d1e88215b478b089bf",
"body": "The Path API allows for proofs that speak about a particular path through an NFA, with constructions that depend on the specific states the path passes through, rather than just the abstract existence of such a path, which is what `evalFrom` computes.\r\n\r\nThis is the part of the API that proved uncontroversial, extracted out of #23929.\r\n\r\n\r\n\n\nCo-authored-by: Maja Kądziołka <maya@compilercrim.es>",
"is_bot": false,
"headline": "feat(Computability/NFA): add a Path API (#25321)",
"author_name": "Maja Kądziołka",
"author_login": "meithecatte",
"committed_at": "2025-06-07T07:26:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "aee234abac64be3d07339c992ca848fcde48bb9f",
"body": null,
"is_bot": false,
"headline": "feat(overview.yml): mention Turing degrees (#25061)",
"author_name": "Tanner Duve",
"author_login": "tannerduve",
"committed_at": "2025-06-07T07:26:44Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5b64b24ed2af77e69f26d7f2f4b76f2baada71bd",
"body": "The TODO on equivalence between regular expressions and DFAs seems to be particularly appealing to new contributors, having spawned multiple competing PRs working towards that goal.\r\n\r\nIt is also one where a new contributor is quite likely to produce a design that is not inline with mathlib's API de\n[…]\nire a lot of guidance, which causes the PRs to languish in review.\r\n\r\nReword the TODO to make it less likely that the situation gets worse.\r\n\r\n\r\n\n\nCo-authored-by: Maja Kądziołka <maya@compilercrim.es>",
"is_bot": false,
"headline": "chore(RegularExpressions): clarify that TODO has pending PRs (#24205)",
"author_name": "Maja Kądziołka",
"author_login": "meithecatte",
"committed_at": "2025-06-07T07:26:43Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "4f54a550f93afebf0f903297f5ab0babd842c3c5",
"body": "Also modify `Int.le_induction` and `Int.le_induction_down` to be like `Nat.le_induction` – `induction n, hn using` syntax can now be used with the first two recursors.\r\n\r\nSee [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Naming.20of.20.60Int.60.20recursors/near/522863583).",
"is_bot": false,
"headline": "chore: better recursor names for `ℤ` (#25555)",
"author_name": "Jeremy Tan Jie Rui",
"author_login": "Parcly-Taxel",
"committed_at": "2025-06-07T06:38:24Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "994033ef9c4b418ad19747aa3589495b60728067",
"body": "zulip discussion: [#new members > EuclideanSpace.single 2 1 ≠ 0](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/EuclideanSpace.2Esingle.202.201.20.E2.89.A0.200/with/522858317)\r\n\r\n\n\nCo-authored-by: Eric Wieser <wieser.eric@gmail.com>",
"is_bot": false,
"headline": "feat: simp lemmas for WithLp eq zero (#25552)",
"author_name": "zhikaip",
"author_login": "zhikaip",
"committed_at": "2025-06-07T02:30:06Z",
"body_truncated": false,
"is_coding_agent": false
}
],
"releases_count": 14,
"commits_last_year": 0,
"latest_release_at": "2025-06-04T13:56:59Z",
"latest_release_tag": "v4.20.1",
"releases_from_tags": true,
"days_since_last_push": 129,
"active_weeks_last_year": 0,
"days_since_latest_release": 418,
"mean_days_between_releases": 5.8
},
"community": {
"has_readme": false,
"has_license": false,
"has_description": false,
"has_contributing": false,
"health_percentage": null,
"has_issue_template": false,
"has_code_of_conduct": false,
"has_pull_request_template": false
},
"ecosystem": {
"packages": []
},
"popularity": {
"forks": 0,
"stars": 0,
"watchers": 0,
"fork_history": {
"days": [],
"complete": true,
"collected": 0,
"total_forks": 0
},
"star_history": {
"days": [],
"complete": true,
"collected": 0,
"total_stars": 0,
"collected_at": null
},
"open_issues_and_prs": 0
},
"ai_readiness": {
"has_nix": false,
"example_dirs": [
"examples"
],
"has_llms_txt": false,
"has_dockerfile": true,
"has_mcp_signal": false,
"bootstrap_files": [
"GNUmakefile"
],
"api_schema_files": [],
"has_devcontainer": true,
"typecheck_configs": [],
"toolchain_manifests": [],
"largest_source_bytes": 24562,
"source_files_sampled": 12,
"oversized_source_files": 0,
"agent_instruction_files": [],
"agent_instruction_max_bytes": null
},
"dependencies": {
"manifests": [],
"advisories": {
"error": null,
"scope": null,
"source": null,
"findings": [],
"collected": false,
"malicious": [],
"truncated": false,
"by_severity": {},
"advisory_count": 0,
"affected_count": 0,
"assessed_count": 0,
"malicious_count": 0,
"assessed_package": null,
"unassessed_count": 0,
"direct_affected_count": 0
},
"ecosystems": [],
"dependencies": [],
"all_dependencies": {
"error": "GitHub dependency-graph SBOM unavailable (404); the dependency graph may be disabled for this repository",
"source": null,
"packages": [],
"collected": false,
"truncated": false,
"total_count": null,
"direct_count": null,
"indirect_count": null
}
},
"maintainership": {
"issues": {
"open_prs": 0,
"merged_prs": 1,
"open_issues": 0,
"closed_ratio": null,
"closed_issues": 0,
"closed_unmerged_prs": 0
},
"bus_factor": 12,
"bot_contributors": 1,
"top_contributors": [
{
"type": "User",
"login": "urkud",
"commits": 1677,
"avatar_url": "https://avatars.githubusercontent.com/u/188813?v=4"
},
{
"type": "User",
"login": "kim-em",
"commits": 1397,
"avatar_url": "https://avatars.githubusercontent.com/u/477956?v=4"
},
{
"type": "User",
"login": "YaelDillies",
"commits": 1369,
"avatar_url": "https://avatars.githubusercontent.com/u/14090593?v=4"
},
{
"type": "User",
"login": "eric-wieser",
"commits": 853,
"avatar_url": "https://avatars.githubusercontent.com/u/425260?v=4"
},
{
"type": "User",
"login": "Ruben-VandeVelde",
"commits": 814,
"avatar_url": "https://avatars.githubusercontent.com/u/65514131?v=4"
},
{
"type": "User",
"login": "joelriou",
"commits": 758,
"avatar_url": "https://avatars.githubusercontent.com/u/37772949?v=4"
},
{
"type": "User",
"login": "grunweg",
"commits": 673,
"avatar_url": "https://avatars.githubusercontent.com/u/10105016?v=4"
},
{
"type": "User",
"login": "Parcly-Taxel",
"commits": 613,
"avatar_url": "https://avatars.githubusercontent.com/u/54175463?v=4"
},
{
"type": "User",
"login": "adomani",
"commits": 500,
"avatar_url": "https://avatars.githubusercontent.com/u/29467745?v=4"
},
{
"type": "User",
"login": "j-loreaux",
"commits": 391,
"avatar_url": "https://avatars.githubusercontent.com/u/8920598?v=4"
}
],
"contributors_sampled": 99,
"top_contributor_share": 0.088
},
"quality_signals": {
"has_ci": true,
"has_tests": true,
"ci_workflows": [
"PR_summary.yml",
"actionlint.yml",
"add_label_from_diff.yaml",
"bench_summary_comment.yml",
"bors.yml",
"bot_fix_style.yaml",
"build.yml",
"build_fork.yml",
"daily.yml",
"dependent-issues.yml",
"discover-lean-pr-testing.yml",
"docker_build.yml",
"label_new_contributor.yml",
"labels_from_comment.yml",
"latest_import.yml",
"lint_and_suggest_pr.yml",
"long_file_report.yml",
"maintainer_bors.yml",
"maintainer_merge.yml",
"merge_conflicts.yml",
"nightly_bump_toolchain.yml",
"nightly_detect_failure.yml",
"nightly_merge_master.yml",
"nolints.yml",
"stale.yml",
"sync_closed_tasks.yaml",
"technical_debt_metrics.yml",
"update_dependencies.yml",
"update_dependencies_zulip.yml",
"zulip_emoji_closed_pr.yaml",
"zulip_emoji_labelling.yaml",
"zulip_emoji_merge_delegate.yaml"
],
"has_docs_dir": true,
"linter_configs": [],
"has_editorconfig": false,
"has_linter_config": false,
"has_precommit_config": false
},
"security_signals": {
"lockfiles": [],
"scorecard": {
"checks": [
{
"name": "Binary-Artifacts",
"score": 10,
"reason": "no binaries found in the repo",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#binary-artifacts"
},
{
"name": "Branch-Protection",
"score": 0,
"reason": "branch protection not enabled on development/release branches",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#branch-protection"
},
{
"name": "CI-Tests",
"score": null,
"reason": "no pull request found",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#ci-tests"
},
{
"name": "CII-Best-Practices",
"score": 0,
"reason": "no effort to earn an OpenSSF best practices badge detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#cii-best-practices"
},
{
"name": "Code-Review",
"score": 0,
"reason": "Found 0/30 approved changesets -- score normalized to 0",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#code-review"
},
{
"name": "Contributors",
"score": 10,
"reason": "project has 35 contributing companies or organizations",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#contributors"
},
{
"name": "Dangerous-Workflow",
"score": 0,
"reason": "dangerous workflow patterns detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#dangerous-workflow"
},
{
"name": "Dependency-Update-Tool",
"score": 10,
"reason": "update tool detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#dependency-update-tool"
},
{
"name": "Fuzzing",
"score": 0,
"reason": "project is not fuzzed",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#fuzzing"
},
{
"name": "License",
"score": 10,
"reason": "license file detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#license"
},
{
"name": "Maintained",
"score": 0,
"reason": "0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#maintained"
},
{
"name": "Packaging",
"score": 10,
"reason": "packaging workflow detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#packaging"
},
{
"name": "Pinned-Dependencies",
"score": 7,
"reason": "dependency not pinned by hash detected -- score normalized to 7",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#pinned-dependencies"
},
{
"name": "SAST",
"score": 0,
"reason": "no SAST tool detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#sast"
},
{
"name": "Security-Policy",
"score": 0,
"reason": "security policy file not detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#security-policy"
},
{
"name": "Signed-Releases",
"score": null,
"reason": "no releases found",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#signed-releases"
},
{
"name": "Token-Permissions",
"score": 0,
"reason": "detected GitHub workflow tokens with excessive permissions",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#token-permissions"
},
{
"name": "Vulnerabilities",
"score": 10,
"reason": "0 existing vulnerabilities detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#vulnerabilities"
}
],
"commit": "efe911a4cad7ab54c187dabca7f8ee633f099be9",
"ran_at": "2026-07-27T22:19:30Z",
"aggregate_score": 3.8,
"scorecard_version": "v5.5.0"
},
"has_codeql_workflow": false,
"has_security_policy": false,
"has_dependabot_config": true
},
"contribution_flow": {
"collected": true,
"ci_last_run_at": "2026-03-20T10:38:01Z",
"oldest_open_prs": [],
"last_merged_pr_at": "2026-02-08T19:59:16Z",
"ci_last_conclusion": "SKIPPED",
"oldest_open_issues": []
}
},
"config": {
"disabled_metrics": [],
"disabled_categories": [],
"disabled_components": {}
},
"source": {
"url": "https://github.com/mattrobball/mathlib4_fork",
"host": "github.com",
"name": "mathlib4_fork",
"owner": "mattrobball"
},
"metrics": {
"overall": {
"key": "overall",
"band": "at_risk",
"name": "Overall health",
"note": "Abandonment Policy applies a 85% multiplier to weighted overall health.",
"notes": [
{
"code": "abandonment_overall_adjustment",
"params": {
"cap": 0,
"pct": 85
}
}
],
"value": 37,
"inputs": {
"security": 38,
"vitality": 28,
"community": 12,
"governance": 75,
"engineering": 56,
"abandonment_cap": null,
"abandonment_state": "at_risk",
"abandonment_multiplier": 85,
"weighted_overall_before_abandonment": 44,
"overall_after_abandonment_multiplier": 37
},
"components": []
},
"categories": [
{
"key": "vitality",
"band": "critical",
"name": "Vitality",
"value": 28,
"weight": 0.22,
"metrics": [
{
"key": "development_activity",
"band": "critical",
"name": "Development activity",
"note": null,
"notes": [],
"value": 10,
"inputs": {
"commits_last_year": 0,
"human_commit_share": 0.97,
"days_since_last_push": 129,
"active_weeks_last_year": 0
},
"components": [
{
"key": "push_recency",
"name": "Push recency",
"detail": "last push 129 days ago",
"points": 9.9,
"status": "partial",
"details": [
{
"code": "push_recency",
"params": {
"days": 129
}
}
],
"max_points": 36
},
{
"key": "commit_cadence",
"name": "Commit cadence",
"detail": "0/52 weeks with commits",
"points": 0,
"status": "missed",
"details": [
{
"code": "commit_cadence_weeks",
"params": {
"weeks": 0
}
}
],
"max_points": 36
},
{
"key": "commit_volume",
"name": "Commit volume",
"detail": "0 commits in the last year",
"points": 0,
"status": "missed",
"details": [
{
"code": "commits_last_year",
"params": {
"count": 0
}
}
],
"max_points": 18
},
{
"key": "openssf_scorecard_maintained",
"name": "OpenSSF Scorecard: Maintained",
"detail": "0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
}
]
},
{
"key": "release_discipline",
"band": "moderate",
"name": "Release discipline",
"note": "Excluded from scoring (no data or not applicable): OpenSSF Scorecard: Signed-Releases. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"openssf_scorecard_signed_releases"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 56,
"inputs": {
"releases_count": 14,
"latest_release_tag": "v4.20.1",
"releases_from_tags": true,
"days_since_latest_release": 418,
"mean_days_between_releases": 5.8
},
"components": [
{
"key": "ships_releases",
"name": "Ships releases",
"detail": "14 version tags (no GitHub releases)",
"points": 16.2,
"status": "partial",
"details": [
{
"code": "version_tags_no_releases",
"params": {
"count": 14
}
}
],
"max_points": 27
},
{
"key": "release_recency",
"name": "Release recency",
"detail": "latest release 418 days ago",
"points": 7.2,
"status": "partial",
"details": [
{
"code": "release_recency",
"params": {
"days": 418
}
}
],
"max_points": 36
},
{
"key": "release_cadence",
"name": "Release cadence",
"detail": "a release every ~5.8 days",
"points": 27,
"status": "met",
"details": [
{
"code": "release_cadence",
"params": {
"gap": 5.8
}
}
],
"max_points": 27
},
{
"key": "openssf_scorecard_signed_releases",
"name": "OpenSSF Scorecard: Signed-Releases",
"detail": "no releases found",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 10
}
]
},
{
"key": "abandonment",
"band": "excellent",
"name": "Abandonment",
"note": null,
"notes": [],
"value": 85,
"inputs": {
"cap": null,
"state": "at_risk",
"guards": [
"no_open_demand"
],
"signals": [
"release_stall",
"scorecard_unmaintained"
],
"red_flag": true,
"multiplier_pct": 85,
"declared_reason": null,
"unverified_reason": null,
"unanswered_open_prs": 0,
"unanswered_open_issues": 0,
"days_since_last_merged_pr": 169,
"days_since_last_human_commit": 411,
"days_since_last_human_commit_is_floor": false
},
"components": [
{
"key": "project_is_still_maintained",
"name": "Project is still maintained",
"detail": "no human commit for 411 days; 2 unmet obligation(s): releases stalled, Scorecard reports it unmaintained",
"points": 85,
"status": "partial",
"details": [
{
"code": "abandonment_flagged",
"params": {
"days": 411,
"count": 2,
"signals": "releases stalled, Scorecard reports it unmaintained"
}
}
],
"max_points": 100
}
]
}
],
"description": "Is the project alive — is code being written and are releases shipping?"
},
{
"key": "community",
"band": "critical",
"name": "Community & Adoption",
"value": 12,
"weight": 0.18,
"metrics": [
{
"key": "popularity",
"band": "critical",
"name": "Popularity & adoption",
"note": null,
"notes": [],
"value": 1,
"inputs": {
"forks": 0,
"stars": 0,
"watchers": 0,
"growth_state": "unverified",
"growth_factor_pct": 100,
"growth_unverified_reason": "no_history"
},
"components": [
{
"key": "stars",
"name": "Stars",
"detail": "0 stars",
"points": 0,
"status": "missed",
"details": [
{
"code": "stars",
"params": {
"count": 0
}
}
],
"max_points": 60
},
{
"key": "forks",
"name": "Forks",
"detail": "0 forks",
"points": 0,
"status": "missed",
"details": [
{
"code": "forks",
"params": {
"count": 0
}
}
],
"max_points": 25
},
{
"key": "watchers",
"name": "Watchers",
"detail": "0 watchers",
"points": 0,
"status": "missed",
"details": [
{
"code": "watchers",
"params": {
"count": 0
}
}
],
"max_points": 15
}
]
},
{
"key": "community_health",
"band": "critical",
"name": "Community health",
"note": null,
"notes": [],
"value": 25,
"inputs": {
"has_readme": false,
"has_license": false,
"has_contributing": false,
"has_issue_template": false,
"has_code_of_conduct": false,
"has_pull_request_template": false
},
"components": [
{
"key": "readme",
"name": "README",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 22.5
},
{
"key": "license",
"name": "License",
"detail": "recognized license (Apache-2.0)",
"points": 22.5,
"status": "met",
"details": [
{
"code": "license_standard",
"params": {}
},
{
"code": "license_spdx",
"params": {
"spdx": "Apache-2.0"
}
}
],
"max_points": 22.5
},
{
"key": "contributing_guide",
"name": "CONTRIBUTING guide",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 18
},
{
"key": "code_of_conduct",
"name": "Code of conduct",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 13.5
},
{
"key": "issue_template",
"name": "Issue template",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.2
},
{
"key": "pr_template",
"name": "PR template",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 6.3
}
]
}
],
"description": "Does the project have users, downloads, attention, and a welcoming setup for contributors?"
},
{
"key": "governance",
"band": "good",
"name": "Sustainability & Governance",
"value": 75,
"weight": 0.24,
"metrics": [
{
"key": "maintainer_resilience",
"band": "excellent",
"name": "Maintainer resilience (bus factor)",
"note": null,
"notes": [],
"value": 98,
"inputs": {
"bus_factor": 12,
"contributors_sampled": 99,
"top_contributor_share": 0.088
},
"components": [
{
"key": "bus_factor",
"name": "Bus factor",
"detail": "12 contributor(s) cover half of all commits",
"points": 54,
"status": "met",
"details": [
{
"code": "bus_factor",
"params": {
"count": 12
}
}
],
"max_points": 54
},
{
"key": "commit_distribution",
"name": "Commit distribution",
"detail": "top contributor authored 9% of commits",
"points": 20.5,
"status": "partial",
"details": [
{
"code": "top_contributor_share",
"params": {
"share": 9
}
}
],
"max_points": 22.5
},
{
"key": "contributor_breadth",
"name": "Contributor breadth",
"detail": "99 contributors",
"points": 13.5,
"status": "met",
"details": [
{
"code": "contributors_sampled",
"params": {
"count": 99
}
}
],
"max_points": 13.5
},
{
"key": "openssf_scorecard_contributors",
"name": "OpenSSF Scorecard: Contributors",
"detail": "project has 35 contributing companies or organizations",
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
},
{
"key": "responsiveness",
"band": "good",
"name": "Issue & PR responsiveness",
"note": "Excluded from scoring (no data or not applicable): Issue resolution. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"issue_resolution"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 72,
"inputs": {
"merged_prs": 1,
"open_issues": 0,
"closed_issues": 0,
"issue_closed_ratio": null,
"closed_unmerged_prs": 0
},
"components": [
{
"key": "issue_resolution",
"name": "Issue resolution",
"detail": "no issues or no data",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_issues_or_data",
"params": {}
}
],
"max_points": 46.75
},
{
"key": "pr_acceptance",
"name": "PR acceptance",
"detail": "1/1 decided PRs merged",
"points": 38.2,
"status": "met",
"details": [
{
"code": "decided_prs_merged",
"params": {
"merged": 1,
"decided": 1
}
}
],
"max_points": 38.25
},
{
"key": "openssf_scorecard_code_review",
"name": "OpenSSF Scorecard: Code-Review",
"detail": "Found 0/30 approved changesets -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 15
}
]
},
{
"key": "stewardship",
"band": "moderate",
"name": "Ownership & stewardship",
"note": "Excluded from scoring (no data or not applicable): Verified domain. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"verified_domain"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 51,
"inputs": {
"followers": 24,
"owner_type": "User",
"is_verified": null,
"owner_login": "mattrobball",
"public_repos": 37,
"account_age_days": 1619
},
"components": [
{
"key": "ownership_backing",
"name": "Ownership backing",
"detail": "personal (user) account",
"points": 10,
"status": "partial",
"details": [
{
"code": "owner_personal",
"params": {}
}
],
"max_points": 30
},
{
"key": "verified_domain",
"name": "Verified domain",
"detail": "not applicable to user accounts",
"points": 0,
"status": "excluded",
"details": [
{
"code": "not_applicable_to_user_accounts",
"params": {}
}
],
"max_points": 20
},
{
"key": "owner_reach",
"name": "Owner reach",
"detail": "24 followers of mattrobball",
"points": 10.1,
"status": "partial",
"details": [
{
"code": "owner_followers",
"params": {
"count": 24,
"login": "mattrobball"
}
}
],
"max_points": 25
},
{
"key": "track_record",
"name": "Track record",
"detail": "37 public repos, account ~4 yr old",
"points": 20.4,
"status": "partial",
"details": [
{
"code": "public_repos",
"params": {
"count": 37
}
},
{
"code": "account_age_years",
"params": {
"years": 4
}
}
],
"max_points": 25
}
]
}
],
"description": "Will the project survive its people — bus factor, responsiveness, who backs it, and package upkeep?"
},
{
"key": "engineering",
"band": "moderate",
"name": "Engineering Quality",
"value": 56,
"weight": 0.2,
"metrics": [
{
"key": "engineering_practices",
"band": "moderate",
"name": "Engineering practices",
"note": "Excluded from scoring (no data or not applicable): OpenSSF Scorecard: CI-Tests. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"openssf_scorecard_ci_tests"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 60,
"inputs": {
"has_ci": true,
"has_tests": true,
"has_editorconfig": false,
"has_linter_config": false,
"has_precommit_config": false
},
"components": [
{
"key": "ci_workflows",
"name": "CI workflows",
"detail": "32 workflow(s)",
"points": 24,
"status": "met",
"details": [
{
"code": "ci_workflows",
"params": {
"count": 32
}
}
],
"max_points": 24
},
{
"key": "tests_present",
"name": "Tests present",
"detail": null,
"points": 24,
"status": "met",
"details": [],
"max_points": 24
},
{
"key": "linter_config",
"name": "Linter config",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 16
},
{
"key": "pre_commit_hooks",
"name": "Pre-commit hooks",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 9.6
},
{
"key": "editorconfig",
"name": ".editorconfig",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 6.4
},
{
"key": "openssf_scorecard_ci_tests",
"name": "OpenSSF Scorecard: CI-Tests",
"detail": "no pull request found",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 20
}
]
},
{
"key": "documentation",
"band": "moderate",
"name": "Documentation",
"note": null,
"notes": [],
"value": 50,
"inputs": {
"topics": [],
"has_wiki": true,
"homepage": "https://leanprover-community.github.io/mathlib4_docs",
"has_readme": false,
"has_docs_dir": true,
"has_description": false
},
"components": [
{
"key": "readme",
"name": "README",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 30
},
{
"key": "documentation_directory",
"name": "Documentation directory",
"detail": null,
"points": 25,
"status": "met",
"details": [],
"max_points": 25
},
{
"key": "documentation_homepage_site",
"name": "Documentation / homepage site",
"detail": "https://leanprover-community.github.io/mathlib4_docs",
"points": 15,
"status": "met",
"details": [],
"max_points": 15
},
{
"key": "repository_description",
"name": "Repository description",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
},
{
"key": "topics",
"name": "Topics",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
},
{
"key": "wiki",
"name": "Wiki",
"detail": null,
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
}
],
"description": "Are baseline engineering and documentation practices in place?"
},
{
"key": "security",
"band": "at_risk",
"name": "Security",
"value": 38,
"weight": 0.16,
"metrics": [
{
"key": "security_posture",
"band": "at_risk",
"name": "Security posture",
"note": "Excluded from scoring (no data or not applicable): CI-Tests, Signed-Releases. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"ci_tests",
"signed_releases"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 38,
"inputs": {
"source": "openssf_scorecard",
"checks_evaluated": 16,
"scorecard_version": "v5.5.0",
"checks_inconclusive": 2,
"scorecard_aggregate": 3.8
},
"components": [
{
"key": "binary_artifacts",
"name": "Binary-Artifacts",
"detail": "no binaries found in the repo",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
},
{
"key": "branch_protection",
"name": "Branch-Protection",
"detail": "branch protection not enabled on development/release branches",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "ci_tests",
"name": "CI-Tests",
"detail": "no pull request found",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 2.5
},
{
"key": "cii_best_practices",
"name": "CII-Best-Practices",
"detail": "no effort to earn an OpenSSF best practices badge detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 2.5
},
{
"key": "code_review",
"name": "Code-Review",
"detail": "Found 0/30 approved changesets -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "contributors",
"name": "Contributors",
"detail": "project has 35 contributing companies or organizations",
"points": 2.5,
"status": "met",
"details": [],
"max_points": 2.5
},
{
"key": "dangerous_workflow",
"name": "Dangerous-Workflow",
"detail": "dangerous workflow patterns detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
},
{
"key": "dependency_update_tool",
"name": "Dependency-Update-Tool",
"detail": "update tool detected",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
},
{
"key": "fuzzing",
"name": "Fuzzing",
"detail": "project is not fuzzed",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "license",
"name": "License",
"detail": "license file detected",
"points": 2.5,
"status": "met",
"details": [],
"max_points": 2.5
},
{
"key": "maintained",
"name": "Maintained",
"detail": "0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "packaging",
"name": "Packaging",
"detail": "packaging workflow detected",
"points": 5,
"status": "met",
"details": [],
"max_points": 5
},
{
"key": "pinned_dependencies",
"name": "Pinned-Dependencies",
"detail": "dependency not pinned by hash detected -- score normalized to 7",
"points": 3.5,
"status": "partial",
"details": [],
"max_points": 5
},
{
"key": "sast",
"name": "SAST",
"detail": "no SAST tool detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "security_policy",
"name": "Security-Policy",
"detail": "security policy file not detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "signed_releases",
"name": "Signed-Releases",
"detail": "no releases found",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 7.5
},
{
"key": "token_permissions",
"name": "Token-Permissions",
"detail": "detected GitHub workflow tokens with excessive permissions",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "vulnerabilities",
"name": "Vulnerabilities",
"detail": "0 existing vulnerabilities detected",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
}
]
},
{
"key": "high_risk_jurisdiction_exposure",
"band": "excellent",
"name": "High-Risk Jurisdiction Exposure",
"note": "Only high-confidence self-published location evidence affects this multiplier. Ambiguous matches are review-only; country evidence is not proof of nationality, citizenship, legal registration, malicious intent, or sanctions status.",
"notes": [
{
"code": "jurisdiction_evidence_limits",
"params": {}
}
],
"value": 100,
"inputs": {
"meaning": "self-published location evidence; not nationality or citizenship",
"red_flag": false,
"exposures": [],
"policy_countries": [
"Russia",
"Iran",
"North Korea"
],
"review_only_matches": 0,
"assessed_self_published_locations": 12
},
"components": [
{
"key": "policy_exposure_multiplier",
"name": "Policy exposure multiplier",
"detail": "no confirmed policy-scope location match",
"points": 100,
"status": "met",
"details": [
{
"code": "jurisdiction_no_match",
"params": {}
}
],
"max_points": 100
}
]
}
],
"description": "Are visible security and supply-chain practices strong, with no malicious dependency and no unresolved high-risk jurisdiction exposure?"
},
{
"key": "ai_readiness",
"band": "moderate",
"name": "AI Readiness",
"value": 51,
"weight": 0,
"metrics": [
{
"key": "ai_agent_context",
"band": "at_risk",
"name": "Agent context & guidance",
"note": null,
"notes": [],
"value": 40,
"inputs": {
"has_llms_txt": false,
"legible_history_share": 1,
"agent_instruction_files": [],
"agent_instruction_max_bytes": null
},
"components": [
{
"key": "agent_instructions",
"name": "Agent instructions",
"detail": "no CLAUDE.md / AGENTS.md / editor rules",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_agent_instructions",
"params": {}
}
],
"max_points": 45
},
{
"key": "machine_readable_docs_llms_txt",
"name": "Machine-readable docs (llms.txt)",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 15
},
{
"key": "legible_commit_history",
"name": "Legible commit history",
"detail": "97 of 97 human commits state their intent (structured subject or explanatory body)",
"points": 40,
"status": "met",
"details": [
{
"code": "legible_history",
"params": {
"legible": 97,
"sampled": 97
}
}
],
"max_points": 40
}
]
},
{
"key": "ai_verify_loop",
"band": "moderate",
"name": "Verify loop (build / test / typecheck)",
"note": null,
"notes": [],
"value": 62,
"inputs": {
"has_nix": false,
"has_tests": true,
"lockfiles": [],
"has_dockerfile": true,
"typed_language": false,
"bootstrap_files": [
"GNUmakefile"
],
"has_devcontainer": true,
"has_linter_config": false,
"typecheck_configs": [],
"agent_commit_share": 0,
"toolchain_manifests": [],
"dependency_bot_commit_share": 0
},
"components": [
{
"key": "one_command_bootstrap",
"name": "One-command bootstrap",
"detail": "GNUmakefile",
"points": 18,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": "GNUmakefile"
}
}
],
"max_points": 18
},
{
"key": "automated_tests",
"name": "Automated tests",
"detail": null,
"points": 22,
"status": "met",
"details": [],
"max_points": 22
},
{
"key": "lint_format_config",
"name": "Lint / format config",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 11
},
{
"key": "static_type_checking",
"name": "Static type checking",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 11
},
{
"key": "reproducible_environment",
"name": "Reproducible environment",
"detail": "devcontainer, Dockerfile",
"points": 10,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": "devcontainer, Dockerfile"
}
}
],
"max_points": 10
},
{
"key": "demonstrated_agent_practice",
"name": "Demonstrated agent practice",
"detail": "no agent-authored commits among the last 100",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_agent_authored_commits",
"params": {
"sampled": 100
}
}
],
"max_points": 10
},
{
"key": "automated_maintenance",
"name": "Automated maintenance",
"detail": "dependency automation configured, none observed in the sampled commits",
"points": 5,
"status": "partial",
"details": [
{
"code": "dependency_bot_config_only",
"params": {}
}
],
"max_points": 8
},
{
"key": "openssf_scorecard_pinned_dependencies",
"name": "OpenSSF Scorecard: Pinned-Dependencies",
"detail": "dependency not pinned by hash detected -- score normalized to 7",
"points": 7,
"status": "partial",
"details": [],
"max_points": 10
}
]
},
{
"key": "ai_code_legibility",
"band": "moderate",
"name": "Code legibility for models",
"note": null,
"notes": [],
"value": 55,
"inputs": {
"primary_language": "Lean",
"largest_source_bytes": 24562,
"source_files_sampled": 12,
"oversized_source_files": 0
},
"components": [
{
"key": "type_checkable_code",
"name": "Type-checkable code",
"detail": "Lean without a type-check config",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_typecheck_config_language",
"params": {
"language": "Lean"
}
}
],
"max_points": 45
},
{
"key": "manageable_file_sizes",
"name": "Manageable file sizes",
"detail": "0/12 source files over 60KB",
"points": 55,
"status": "met",
"details": [
{
"code": "oversized_source_files",
"params": {
"kb": 60,
"sampled": 12,
"oversized": 0
}
}
],
"max_points": 55
}
]
},
{
"key": "ai_interfaces",
"band": "at_risk",
"name": "Machine-readable interfaces",
"note": null,
"notes": [],
"value": 40,
"inputs": {
"example_dirs": [
"examples"
],
"has_mcp_signal": false,
"api_schema_files": []
},
"components": [
{
"key": "api_schema_openapi_graphql_proto",
"name": "API schema (OpenAPI/GraphQL/proto)",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 40
},
{
"key": "mcp_server",
"name": "MCP server",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 20
},
{
"key": "runnable_examples",
"name": "Runnable examples",
"detail": "examples",
"points": 40,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": "examples"
}
}
],
"max_points": 40
}
]
}
],
"description": "How well is the repo equipped to be developed and maintained with AI coding agents? An independent, experimental badge — weight 0.0, so it is surfaced on its own and does not affect the overall health score."
}
],
"metrics_version": "1.13.0"
},
"warnings": [
"Community profile unavailable",
"GitHub dependency-graph SBOM unavailable (404); the dependency graph may be disabled for this repository"
],
"report_type": "repository",
"generated_at": "2026-07-27T22:19:55.674565Z",
"schema_version": "0.27.0",
"badge_url": "https://raw.githubusercontent.com/inspect-software/badges/main/v1/m/mattrobball/mathlib4_fork.svg",
"full_name": "mattrobball/mathlib4_fork",
"license_state": "standard",
"license_spdx": "Apache-2.0"
}Bewertungen sind Signale, keine Garantien. Sie spiegeln öffentlich sichtbare Praxis auf GitHub wider — kein Code-Audit und keine Sicherheitsgarantie.
Fehlende Daten werden ausgeschlossen und die Gewichte neu normiert, nie als null bewertet. Die Methodik ist versioniert und offen: Metriken v1.13.0, Schema v0.27.0 — vollständige Methodik · Metriken-Wiki.
Wie ein einzelnes Ergebnis im Gesamtregister steht: aggregierte Statistiken.