Skip to content

[WIP] Quantizing Pythagorean triples formalization - #4

Draft
Lemmy00 wants to merge 1 commit into
mainfrom
milikic/wip-quantizing-pythagorean-triples
Draft

[WIP] Quantizing Pythagorean triples formalization#4
Lemmy00 wants to merge 1 commit into
mainfrom
milikic/wip-quantizing-pythagorean-triples

Conversation

@Lemmy00

@Lemmy00 Lemmy00 commented Jun 24, 2026

Copy link
Copy Markdown
Member

Summary

  • Reintroduces QuantizingPythagoreanTriples as an isolated WIP formalization branch.
  • Keeps this unfinished project out of the public-ready main cleanup until the remaining theorem skeletons are proved.

Current State

  • Builds with sorry warnings.
  • Known remaining proof obligations: 22 project-local sorrys.
  • Keeps the paper's open unimodality_conjecture as an explicit axiom.

Validation

  • cd QuantizingPythagoreanTriples && lake exe cache get && lake build Pythagore2

@Lemmy00
Lemmy00 changed the base branch from milikic/public-readme-completed-projects to main June 24, 2026 01:47
@Lemmy00
Lemmy00 force-pushed the milikic/wip-quantizing-pythagorean-triples branch from f312365 to 24bc842 Compare June 24, 2026 02:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant