Skip to the content

Math 2.0

Resources / preprint

A Lean formalisation of the disproof of Ramaekers's conjecture E215DFNY09

URI	`m2://res/E215DFNY09`
Kind	preprint
Creators	Jeremy Tan
Date	2026-10-12
MSC	11-XX
Subjects	arxiv math.NT, arxiv cs.LO
Scope	in

Expressions

e1: version, preprint

Language	en
Date	2026-10-12
Ids	arXiv 2610.16323, zbl_id 903208868

Items in this resource

The mentions of the inventory that name this resource. Each name links to the card of its inventory row.

Item	Kind	Where	Source
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Common/PrimeChain.lean\#L138}{\Verb\|strongSSC\_chainTup\|	statement	lemma Lemma	arxiv
3QKWFYQ0MC	definition	definition Definition	arxiv
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Odd/Subsum.lean\#L215}{\Verb\|OddCase.strongSSC\_tup\|	statement	lemma Lemma	arxiv
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Common/SubsumCondition.lean\#L199}{\Verb\|pair\_of\_sum\_natAbs\_lt\|	statement	corollary Corollary	arxiv
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Odd/Main.lean\#L155}{\Verb\|quality\_factorFreeTuples\_ge\_of\_odd\_of\_disjoint\|	statement	theorem Theorem	arxiv
EEDFR6X7N9	statement	theorem	arxiv
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Common/VWPair.lean\#L258}{\Verb\|strongSSC\_vwTup\|	statement	lemma Lemma	arxiv
JHK1RF2KDH	definition	definition	arxiv
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Common/SubsumCondition.lean\#L229}{\Verb\|strongSSC\_tupReduce\|	statement	lemma Lemma	arxiv
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/General/Main.lean\#L110}{\Verb\|quality\_factorFreeTuples\_ge\|	statement	theorem Theorem	arxiv
S7CT20SQ06	definition	definition Definition	arxiv
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Four.lean\#L331}{\Verb\|quality\_ramaekersTuples\_four\_ge\|	statement	theorem Theorem	arxiv
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Common/VWPair.lean\#L167}{\Verb\|VWPair.of\|}, \href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Common/VWPair.lean\#L176}{\Verb\|VWPair.of\_coprime\|	statement	lemma Lemma	arxiv
\href{https://github.com/Parcly-Taxel/Redhill/blob/arxiv-fixed/Redhill/Common/SubsumCondition.lean\#L181}{\Verb\|of\_sum\_natAbs\_lt\|	statement	lemma Lemma	arxiv

Catalogue records

arxiv: 2610.16323 (work)
arxiv_text: 2610.16323 (work)
zbmath_search: 903208868 (work)