Main theorem currently proves `True`, not `P = NP` · Issue #1 · TiruArt/Pedigree-Polytopes-Lean4 · GitHub
//voltron/issues_fragments/issue_layout" data-turbo-transient="true" />
Skip to content
Search or jump to...
Search code, repositories, users, issues, pull requests...
-->
Search
Clear
Search syntax tips
Provide feedback
--><br>We read every piece of feedback, and take your input very seriously.
Include my email address so I can be contacted
Cancel
Submit feedback
Saved searches
Use saved searches to filter your results more quickly
-->
Name
Query
To see all available qualifiers, see our documentation.
Cancel
Create saved search
Sign in
//voltron/issues_fragments/issue_layout;ref_cta:Sign up;ref_loc:header logged out"}"<br>Sign up
Appearance settings
Resetting focus
You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.
Dismiss alert
{{ message }}
TiruArt
Pedigree-Polytopes-Lean4
Public
Notifications<br>You must be signed in to change notification settings
Fork
Star
Main theorem currently proves True, not P = NP #1
New issue<br>Copy link
New issue<br>Copy link
Open
Open<br>Main theorem currently proves True, not P = NP#1
Copy link
Description
log2cn<br>opened on Jun 3, 2026
Issue body actions
N_PEqualsNP.lean defines:
def P_equals_NP : Prop := True<br>def SAT_in_P : Prop := True
So the theorem
theorem p_equals_np (n : ℕ) (hn : 5 ≤ n) : P_equals_NP
does not prove a formalized P = NP statement. It proves True.
Reactions are currently unavailable
Metadata<br>Metadata<br>Assignees
No one assigned
Labels
No labelsNo labels
Projects
No projects
Milestone
No milestone
Relationships
None yet
Development
No branches or pull requests
Issue actions
You can’t perform that action at this time.