openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance

Source · Project

Cite & export
Open this versionExport record · JSONRecord detailsReport a correction

Kent · AI-augmented BSD research substrate

Owen P. Kent (repository owner)

Project documentation
View project ↗

Reading source record 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1. This record is retained from earlier public citations. View default cited record →

Overview

Kent · AI-augmented BSD research substrate

Individual project documentation and code; no accepted proof of BSD is asserted by this curation.

1 cited passage ↓1 problem ↓Record 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1 ↓

Passages

The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.

Passage 1 · OpenMath paraphrasePermalink

Pinned README, PHASE_STATE.md and lean/BSD/RankEquality.lean

This individual AI-augmented research project reports numerical experiments and proof-search scaffolding. Its phase record states that Lean verification has not started; RankEquality.lean contains sorry targets.

Read at source ↗2 recorded uses ↓
Passage details

Passage ID: birch-and-swinnerton-dyer-conjecture:bsd-ai-project-kent:v1

Source item: Pinned README, PHASE_STATE.md and lean/BSD/RankEquality.lean

Source record: kent-bsd-project@0e9519aaeb5c8b8c524f95925eecb970d86bc5b1

Used in

Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.

Birch and Swinnerton-Dyer conjecture →

Problem publication v4

Problem context · 2 citations

Research activity

AI-assisted exploration · code and Lean targets

This individual AI-augmented research project reports numerical experiments and proof-search scaffolding. Its phase record states that Lean verification has not started; RankEquality.lean contains sorry targets.

No new BSD theorem, complete formal proof or OpenMath-verified execution is established by this project citation. Its rank-two regulator identity remains conjectural in the project’s own notes.

View in problem →

Question

Birch and Swinnerton-Dyer conjecture

View in problem →

Files

Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.

Project notes

Project phase and limitations ↗

Source-reported evidence

External evidence linked; no OpenMath execution or independent reproduction is asserted.

Resource revision: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1

Code

Computational experiments ↗

No OpenMath execution recorded

External evidence linked; no OpenMath execution or independent reproduction is asserted.

Resource revision: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1

Formal code

Lean rank-equality targets ↗

Statement only · proof placeholder

The inspected weakBSD and low-rank theorem bodies contain sorry. This is a target skeleton, not a completed formal proof.

Resource revision: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1

Credits

Recorded authorship

Owen P. Kent (repository owner)

AI involvement reported by the source

README calls the program AI-augmented and contains Claude agent specifications. A precise model version and independently assessed division of labor are not supplied.

Versions

OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.

  1. 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1Observed Oct 10, 2026 · used in current publications

    Kent · AI-augmented BSD research substrate

  2. Kent · AI-augmented BSD research substrate

Record details
Source ID
kent-bsd-project
Record ID
kent-bsd-project@0e9519aaeb5c8b8c524f95925eecb970d86bc5b1
Recorded title
Kent · AI-augmented BSD research substrate
Revision
0e9519aaeb5c8b8c524f95925eecb970d86bc5b1
Observed
Oct 10, 2026
Source updated
Jun 14, 2026
Content SHA-256
Not recorded
Update method
Manual source and revision check; recheck upstream before a new publication.
Identifier policy
Stable bibliographic identifier and explicit revision; theorem locators belong to source entries.
Check interval
90 days
Rights
metadata-link
License
Links and original OpenMath paraphrases only; upstream license governs external files.

No upstream full text or code is republished by this record.

Source terms ↗