Request for Feedback: Lean 4 Proof related to P=NP

Stream: Program verification

[Essam Abadir]

This is my first time coding in Lean. My proof compiles and checks out but I'd love to hear feedback as to whether anything I did was invalid, nonstandard, libraries I should have used, etc.. Happy to take any / all critiques on the math as well. Full repository with accompanying written paper at: https://github.com/eabadir/PprobablyEqualsNP

import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic -- For log base 2
import Mathlib.Data.List.Basic -- For List.sum
import Mathlib.Data.Set.Defs -- For Set type used by P and NP
-- Using placeholder axioms for complexity theory results not readily available
-- or easy to formalize at this level (like poly-time reduction transitivity).

open Classical

namespace PnPProofDetailedV2

/-!
Section 1: Foundational Definitions (Complexity, SAT, Entropy)
-/

-- Basic Types and Complexity Classes
axiom Word : Type
instance : Inhabited Word := ⟨sorry⟩ -- Give Word a default value
def Lang : Type := Word → Prop -- A language is a property of words

axiom Machine : Type -- Abstract notion of a Turing Machine or equivalent
axiom compute (m : Machine) (w : Word) : Option Word -- Machine computation
axiom timeComplexity (m : Machine) (w : Word) : Nat -- Time cost
axiom wordLength (w : Word) : Nat -- Input size measure

axiom successWord : Word -- Special word indicating acceptance
axiom combineInput (input cert : Word) : Word -- Combining input and certificate for NP

-- Polynomial Time Definitions
def PolyTime (f : Nat → Nat) : Prop :=
  ∃ (c k : Nat), ∀ n, f n ≤ c * n^k + c

def RunsInPolyTime (m : Machine) : Prop :=
  ∃ (p : Nat → Nat), PolyTime p ∧ ∀ w, timeComplexity m w ≤ p (wordLength w)

-- Complexity Class P
def P : Set Lang :=
  { L | ∃ (m : Machine), RunsInPolyTime m ∧
         ∀ w, L w ↔ compute m w = some successWord }

-- Complexity Class NP
def NP : Set Lang :=
  { L | ∃ (m : Machine) (p : Nat → Nat), PolyTime p ∧ RunsInPolyTime m ∧
         ∀ w, L w ↔ ∃ (cert : Word), wordLength cert ≤ p (wordLength w) ∧
                        compute m (combineInput w cert) = some successWord }

-- Polynomial Time Reducibility
def PolyTimeReducible (L1 L2 : Lang) : Prop :=
  ∃ (f : Word → Word) (m : Machine), RunsInPolyTime m ∧
    (∀ w, compute m w = some (f w)) ∧
    (∀ w, L1 w ↔ L2 (f w))

infix:50 " <=p " => PolyTimeReducible -- Notation for reduction

axiom polyTimeReducible_trans {L1 L2 L3 : Lang} :
  (L1 <=p L2) → (L2 <=p L3) → (L1 <=p L3)

-- NP-Completeness Definition
def NPComplete (L : Lang) : Prop :=
  L ∈ NP ∧
  ∀ L' ∈ NP, L' <=p L

-- Circuits and SAT (Boolean Satisfiability Problem)
axiom Circuit : Type
axiom encodeCircuit (c : Circuit) : Word
axiom decodeCircuit (w : Word) : Option Circuit
axiom evalCircuit (c : Circuit) (assignment : Word) : Bool

def SAT_problem : Lang :=
  fun w_c =>
    ∃ c ass, decodeCircuit w_c = some c ∧ evalCircuit c ass = true

axiom CookLevin_inNP   : SAT_problem ∈ NP
axiom CookLevin_hard   : ∀ (L : Lang), L ∈ NP → L <=p SAT_problem

lemma CookLevin : NPComplete SAT_problem := by
  constructor
  · exact CookLevin_inNP
  · intro L hL; exact CookLevin_hard L hL


noncomputable def ShannonEntropy (p : List Real) : Real :=
  - (p.map (fun pi => if pi > 0 then pi * (Real.log pi / Real.log 2) else 0)).sum

axiom ShannonEntropyProblem : Lang

/-!
Section 2: Modeling Physics and Its Properties
-/

axiom PhysicalSystemDesc : Type
axiom IsPhysicalSystem (desc : PhysicalSystemDesc) : Prop
axiom decodeDesc (w : Word) : Option PhysicalSystemDesc
axiom PhysicalSystemProperty (desc : PhysicalSystemDesc) (h_phys : IsPhysicalSystem desc) : Prop

def PhysicalSystemEntropyProblem : Lang :=
  fun w =>
    ∃ (desc : PhysicalSystemDesc) (h_phys : IsPhysicalSystem desc),
      decodeDesc w = some desc ∧
      PhysicalSystemProperty desc h_phys

/-- Rota's Entropy Theorem (RET): Physics entropy reduces to scaled Shannon Entropy. Full derivation of RET is available in the paper, or, available online Rota's unpublished textbook at:
https://archive.org/details/GianCarlo_Rota_and_Kenneth_Baclawski__An_Introduction_to_Probability_and_Random_Processes/page/n367/mode/2up
-/
axiom RET_Reduction_PhysicsEntropy_to_ShannonEntropy : PhysicalSystemEntropyProblem <=p ShannonEntropyProblem

/-- Shannon Coding Theorem: Coding Shannon Entropy is in P O(N log N). -/
axiom ShannonEntropyInPbyShannonCoding : ShannonEntropyProblem ∈ P

axiom reduction_in_P {L1 L2 : Lang} : (L1 <=p L2) → L2 ∈ P → L1 ∈ P

/-- Physics problem is in P via reduction to Shannon Entropy (which is in P). -/
lemma PhysicsProblemIsInP : PhysicalSystemEntropyProblem ∈ P := by
  exact reduction_in_P RET_Reduction_PhysicsEntropy_to_ShannonEntropy ShannonEntropyInPbyShannonCoding

/-!
Section 3: Deriving Physics NP-Completeness
Establishing Reductions and Membership
-/

-- Auxiliary problems and reductions
axiom ProgramProblem : Lang
axiom CircuitProblem : Lang
axiom ShannonEntropyProblemToProgram : ShannonEntropyProblem <=p ProgramProblem
axiom ProgramToCircuitProblem : ProgramProblem <=p CircuitProblem
axiom CircuitProblemToSAT : CircuitProblem <=p SAT_problem

/-- Physics reduces to SAT (via Shannon -> Program -> Circuit -> SAT chain). -/
lemma Physics_to_SAT_Reduction : PhysicalSystemEntropyProblem <=p SAT_problem := by
  have r1 := RET_Reduction_PhysicsEntropy_to_ShannonEntropy
  have r2 := ShannonEntropyProblemToProgram
  have r3 := ProgramToCircuitProblem
  have r4 := CircuitProblemToSAT
  exact polyTimeReducible_trans (polyTimeReducible_trans (polyTimeReducible_trans r1 r2) r3) r4

axiom reducible_in_NP {L1 L2 : Lang} : (L1 <=p L2) → L2 ∈ NP → L1 ∈ NP

/-- Physics ∈ NP (Membership Part of NP-Completeness).
    Derived via the reduction `Physics <=p SAT` and `SAT ∈ NP`. -/
lemma PhysicalSystemEntropyProblemInNP : PhysicalSystemEntropyProblem ∈ NP := by
  exact reducible_in_NP Physics_to_SAT_Reduction CookLevin.1

/-- Axiom: A physical system can realize/encode SAT computations.
    (e.g., Electrons behaving on a substrate designed as a logic circuit).
    This provides the reduction *from* SAT *to* the physical system. -/
axiom Electrons_On_Circuits_Is_Physical_SAT : SAT_problem <=p PhysicalSystemEntropyProblem


/-- Physics problem is NP-complete. -/
lemma PhysicsIsNPComplete : NPComplete PhysicalSystemEntropyProblem := by
  constructor
  · -- Membership: Proven above via reduction TO SAT.
    exact PhysicalSystemEntropyProblemInNP
  · -- NP-Hardness: Show any L ∈ NP reduces to PhysicalSystemEntropyProblem.
    intro L hL -- Assume L is an arbitrary language in NP (hL : L ∈ NP).
    -- Goal: Show L <=p PhysicalSystemEntropyProblem

    -- Step 1: Every L ∈ NP reduces to SAT (by Cook-Levin NP-Hardness).
    have h_L_reduces_to_SAT : L <=p SAT_problem := CookLevin.2 L hL

    -- Step 2: SAT reduces to the PhysicalSystemEntropyProblem (by the new axiom).
    have h_SAT_reduces_to_Physics : SAT_problem <=p PhysicalSystemEntropyProblem :=
      Electrons_On_Circuits_Is_Physical_SAT -- Use the new axiom here

    -- Step 3: Chain the reductions using transitivity.
    -- L <=p SAT_problem  and  SAT_problem <=p PhysicalSystemEntropyProblem  implies  L <=p PhysicalSystemEntropyProblem
    exact polyTimeReducible_trans h_L_reduces_to_SAT h_SAT_reduces_to_Physics

-- Bidirectional reductions between SAT and Physics
-- This is a corollary of the NP-Completeness of both problems.
lemma SAT_is_NPC_and_Physics_is_NPC :
  NPComplete SAT_problem ∧ NPComplete PhysicalSystemEntropyProblem := by
  constructor
  · exact CookLevin
  · exact PhysicsIsNPComplete -- Use the lemma just proved

-- Define notation for bidirectional polynomial-time reducibility
infix:50 " <->p " => fun L1 L2 => (L1 <=p L2) ∧ (L2 <=p L1)

/-- lemma: If two languages are NP-complete, they are poly-time equivalent. -/
lemma NPComplete_problems_are_polyTime_equivalent {L1 L2 : Lang} :
  NPComplete L1 → NPComplete L2 → (L1 <->p L2) :=
by
  intro h_L1_npc h_L2_npc
  constructor
  · exact h_L2_npc.2 L1 h_L1_npc.1 -- L1 ∈ NP reduces to L2 (hard)
  · exact h_L1_npc.2 L2 h_L2_npc.1 -- L2 ∈ NP reduces to L1 (hard)

/-- Corollary: SAT and Physics are bidirectionally reducible because both are NP-Complete. -/
lemma SAT_Physics_bidirectional_reduction :
  SAT_problem <->p PhysicalSystemEntropyProblem :=
by
  have h_sat_npc := CookLevin
  have h_phys_npc := PhysicsIsNPComplete -- Now relies on a sound proof
  exact NPComplete_problems_are_polyTime_equivalent h_sat_npc h_phys_npc

-- We can extract the specific reductions if needed
lemma SAT_to_Physics_derived : SAT_problem <=p PhysicalSystemEntropyProblem :=
  SAT_Physics_bidirectional_reduction.1

lemma Physics_to_SAT_derived : PhysicalSystemEntropyProblem <=p SAT_problem :=
  SAT_Physics_bidirectional_reduction.2


/-!
Section 4: Deriving NP-Completeness and the Contradiction (Steps j, k, l)
-/

axiom P_and_NPComplete_implies_P_eq_NP (L : Lang) :
  L ∈ P → NPComplete L → P = NP

-- Main Theorem: Assuming P ≠ NP leads to a contradiction.
theorem P_eq_NP_from_Physics (h_p_ne_np : P ≠ NP) : False := by
  -- 1. The physics problem is in P (Derived from Rota + Shannon Coding efficiency)
  have hPhys_in_P : PhysicalSystemEntropyProblem ∈ P := PhysicsProblemIsInP

  -- 2. The physics problem is NP-Complete (Proven above using both reduction directions)
  have hPhys_is_NPComplete : NPComplete PhysicalSystemEntropyProblem := PhysicsIsNPComplete

  -- 3. Apply the standard complexity result: If a problem is in P and NP-Complete, then P = NP.
  have h_p_eq_np : P = NP :=
    P_and_NPComplete_implies_P_eq_NP PhysicalSystemEntropyProblem hPhys_in_P hPhys_is_NPComplete

  -- 4. This conclusion (P = NP) contradicts the initial assumption (P ≠ NP).
  exact h_p_ne_np h_p_eq_np


end PnPProofDetailedV2
/- Copyright (c) 2025 Essam Abadir, Distributed under the DeSciX Community License.-/

[Andrés Goens]

I'm not an expert on computability theory and didn't look at it very carefully, but it does strike as notable that you've added a lot of axioms. Not sure what the community is you want to target/get feedback from, but I would imagine the mathematical and theoretical computer science communities at large will not consider your proof reasonable if you've added a bunch of axioms, I'd recommend not adding any axioms. It looks like a lot of things you have there should be definitions, or variables, etc instead.

[Essam Abadir]

Thank you. Are there conventions for using past proven results such as
Shannon’s Coding Theorem? Are those normally definitions instead of axioms?

[Aaron Liu]

Usually, we want to have no axioms in our code (except for the few builtin ones)

[suhr]

More generally, whether you assume a value of some type, there's a question whether the type is inhabited. So when you prove something like H → P = NP, one may wonder if H is inhabited (or true).

An axiom is essentially a global assumption, so writing axiom h: H is like appending H to assumptions of all theorems that use that axiom.

Also, if there are some useful definitions in the Mathlib, it would be wise to use them, so other people would not have to wonder if your definitions of P and NP match the conventional ones.

[Mario Carneiro]

This proof boils down to the following three claims:

/-- Axiom: A physical system can realize/encode SAT computations.
    (e.g., Electrons behaving on a substrate designed as a logic circuit).
    This provides the reduction *from* SAT *to* the physical system. -/
axiom Electrons_On_Circuits_Is_Physical_SAT : SAT_problem <=p PhysicalSystemEntropyProblem

/-- Rota's Entropy Theorem (RET): Physics entropy reduces to scaled Shannon Entropy. Full derivation of RET is available in the paper, or, available online Rota's unpublished textbook at:
https://archive.org/details/GianCarlo_Rota_and_Kenneth_Baclawski__An_Introduction_to_Probability_and_Random_Processes/page/n367/mode/2up
-/
axiom RET_Reduction_PhysicsEntropy_to_ShannonEntropy : PhysicalSystemEntropyProblem <=p ShannonEntropyProblem

/-- Shannon Coding Theorem: Coding Shannon Entropy is in P O(N log N). -/
axiom ShannonEntropyInPbyShannonCoding : ShannonEntropyProblem ∈ P

Certainly, it follows from these three assumptions that P = NP. I don't know what are the shannon entropy problem and the physical system entropy problem, but the result here suggests that you should really dig into these because at least one of these assumptions is probably faulty.

[Essam Abadir]

Thank you. This is all very helpful.

I’ve put some effort into refactoring and moving all fundamental results and definitions from complexity and information theory into a separate definitions file. I’ll look around but if anyone knows of modules that contain generally accepted code for things like the Cook-Levin theorem please let me know.

As Mario says, it then boils to one of those three axioms. Shannon’s Coding Theorem, that any system characterized by Shannon Entropy is codeable with series yes/no questions on the order of n log n, is a foundational proof in information theory. Rota’s Entropy Theorem was taught it for decades at MIT by Prof. Gian-Carlo Rota, a giant in the field of Probability Theory, as the foundational result proved in his class - that physics entropies (Bose-Einstein, Fermi-Dirac, Maxwell-Boltzmann) are mathematically scaled forms of Shannon Entropy ... and it is indeed a very key result. Sadly, despite being taught to generations of MIT mathematics students, Rota's Entropy Theorem seems never to have been formally published ... here is a link to it in his unpublished manuscript posted by one of his students https://archive.org/details/GianCarlo_Rota_and_Kenneth_Baclawski__An_Introduction_to_Probability_and_Random_Processes/page/n367/mode/2up.

I’m working on putting the whole derivation of Rota's Entropy Theorem into Lean but it is seriously pushing the level of my Lean skills. I've checked it in to the repository if anyone is interested / expert https://github.com/eabadir/PprobablyEqualsNP. Currently hitting an issue 0.0 not being acceptable as 0. I’ll post a code question on it separately.

I don't think I can get down to zero axioms though. The last axiom, that electrons traversing a computer circuit is the physical circuit satisfiability SAT problem, seems to be a tautology worthy of an axiom.

[Mario Carneiro]

Note, people will not really fully accept this proof until it has zero axioms. But I think it's fine to be exploring these concepts in lean using axiom. I just suggest you refrain from announcing that you've proved P = NP until you actually have no assumptions and lean is not reporting errors, and even then it's going to draw an extreme level of skepticism and it is more tactful to say you are working on a proof of shannon's coding theorem and/or Rota's entropy theorem rather than leading with P=NP.

[Mario Carneiro]

I don't think I can get down to zero axioms though. The last axiom, that electrons traversing a computer circuit is the physical circuit satisfiability SAT problem, seems to be a tautology worthy of an axiom.

If you think this is unformalizable, then this is actually the most important part to start with. If I understand your conundrum correctly, "electrons traversing a computer circuit" can probably just be replaced by "the circuit satisfiability SAT problem" for the purposes of the proof. This axiom on its own has no proving power; the reason it features in the proof is because you have a reduction of it to the shannon entropy problem, and perhaps you can just skip the unformalizable middle man and prove SAT_problem <=p ShannonEntropyProblem directly. (Or fail to do so, but learn a lot in the process.)

[Essam Abadir]

Thanks, this has been quite helpful and great suggestions which I’ll
incorporate.

I must say though, being new to Lean, it is very counter to my intuition to
not have axioms so I’d love to get a better understanding.

Axioms as normally discussed are the very foundation of formal systems and
any formal argument. To my knowledge you can’t have one without the other,
every proof has them either out in the open or hidden away.

Does Lean syntactically use the word axiom in a different way or is there
something I am misunderstanding understanding about the language?

[Shreyas Srinivas]

These axioms make no sense:

axiom Word : Type
instance : Inhabited Word := ⟨sorry⟩ -- Give Word a default value
def Lang : Type := Word → Prop -- A language is a property of words

axiom Machine : Type -- Abstract notion of a Turing Machine or equivalent
axiom compute (m : Machine) (w : Word) : Option Word -- Machine computation
axiom timeComplexity (m : Machine) (w : Word) : Nat -- Time cost
axiom wordLength (w : Word) : Nat -- Input size measure

axiom successWord : Word -- Special word indicating acceptance
axiom combineInput (input cert : Word) : Word -- Combining input and certificate for NP

[Shreyas Srinivas]

and then there is this:

-- Polynomial Time Definitions
def PolyTime (f : Nat → Nat) : Prop :=
  ∃ (c k : Nat), ∀ n, f n ≤ c * n^k + c

You are really just defining asymptotics for polynomial functions here

[Shreyas Srinivas]

Then you define the following:

def RunsInPolyTime (m : Machine) : Prop :=
  ∃ (p : Nat → Nat), PolyTime p ∧ ∀ w, timeComplexity m w ≤ p (wordLength w)

which is meaningless since you haven't actually provided definitions for timeComplexity and wordLength

[Shreyas Srinivas]

I could go on: But you have stubbed out everything important as an axiom

[Shreyas Srinivas]

including important definitions

[suhr]

I'd just like to interject for a moment. What you’re referring to as ZFC, is in fact, FOL/ZFC, or as I’ve recently taken to calling it, first order logic plus set axioms. ZFC is not a foundation of mathematics unto itself, but rather a set of axioms of a fully functioning first order theory made useful by the logical connectives, quantifiers and vital set of inference rules composing a full formal system as defined by sequent calculus.

A formal system is a set of inference rules that guide how one judgements (conclusions) are derived from other judgements (premises). Some systems, like ZFC or ETCS, are based on inference rules of first-order logic (for example, natural deduction). But these rules do not say anything about things like sets, so you need a whole set of axioms in order to say something.

In contrast, dependent type theories like one used by Lean are not based on first-order logic. They are theories of constructions. A proof is merely a special case of a mathematical construction. Because of that, dependent type theories can be usable without any axioms at all: all you need is already made possible by inference rules. Though, Lean still adds some extra axioms to make life easier.

Whether you use Lean or anything else, you should not add arbitrary axioms without justification, because they can make your theory inconsistent. So if you use ZFC you only use axioms of ZFC, if you use Lean, you only use axioms from the standard library.

[Shreyas Srinivas]

A definition is meaningless without semantic content (the body of the definition at least)

[Shreyas Srinivas]

I mean what stops you from claiming that this implies PSPACE != NPSPACE by renaming some of your axioms (This is false btw, which is my point; you can write false statements like this)

Edit note : As Henrik pointed out below the previous version had an egregious error of comparing L and NL instead

[Henrik Böving]

Shreyas Srinivas said:

(This is false btw, which is my point; you can write false statements like this)

It's not false, just unknown. What is known is that there exists a quadratic reduction of any problem in NL to L (Savitch's theorem) but that does not make them disjoint or equal.

[Essam Abadir]

I appreciate everyone's thoughtful feedback, and I’d like to clarify a central philosophical and practical point raised in this discussion.

As a new Lean user, this discussion seem to suggest two extremes: either Lean contains a complete set of axioms capable of proving anything that's provable, or every proof must regress to an exhaustive first-principles derivation—akin to Russell and Whitehead’s infamous 360-page proof that 1+1=2.

The first scenario—having a complete and sufficient set of axioms—is explicitly ruled out by Gödel’s Incompleteness Theorems, which demonstrate that no consistent, sufficiently rich formal system can prove all truths expressible within it. Thus, expecting Lean, or indeed any formal system, to contain such completeness would seem paradoxical. Furthermore, Russell’s paradox illustrates the risk inherent in naive axiomatics, underscoring why Lean’s axiomatic approach should be valid.

The second scenario—requiring every proof to painstakingly start from foundational logic—defeats the purpose of formalization entirely. Lean’s utility arises precisely from building on well-established theorems and results, enabling practical and concise proofs rather than exhaustive regressions.

My hope in looking at Lean, and formal verification tools in general, was that it would sit thoughtfully between these extremes. That they would rely on a core set of axioms and inference rules, augmented by carefully vetted libraries of established mathematical results. When these standard results (e.g., Cook-Levin, Shannon Coding, and others foundational to computational complexity and information theory) are already proven and accepted, we ideally reference or formalize these results explicitly rather than introducing them as arbitrary axioms.

For precisely these reasons, I have asked multiple times for guidance on generally accepted libraries or packages that provide foundational definitions and results in complexity theory. Attempting to define everything from first principles or redoing well-established proofs such as Shannon's Coding Theorem would only introduce unnecessary error, obfuscation, and complexity into the proof.

Regarding the nature of Lean as a dependent type system, I do not see how it exempts Lean from formal logic. Indeed, dependent type theory itself is a formal logic system—a constructive logic system with additional structure. Lean's type-theoretic foundation is not outside formal logic; rather, it is a well-defined, rigorous subset of it, designed to facilitate both foundational clarity and practical proof management.

Your critique about my liberal use of axioms is fair and well-taken. My intent, especially as someone new to Lean, was to first outline clearly the theoretical landscape of the proof. Now, guided by your feedback, I'm actively working to convert those axioms which are "new" and further definable (such as Rota's Entropy Theorem) into explicit, verifiable theorems and definitions within Lean’s framework, ideally leveraging established libraries and community-accepted definitions.

I just don't see how the complete absence of axioms is practically achievable (as even Lean’s minimal kernel has axiomatic underpinnings), but definitely do understand the goal is always to minimize assumptions by leveraging formally proven, established results. I would hope this strikes the necessary balance between foundational rigor and practical usability, respecting both Gödel’s constraints and Russell’s cautionary lessons.

Again, I VERY MUCH appreciate everyone's input. I look forward to refining the approach. I'm personally most interested at the moment in porting Rota's Entropy Theorem into Lean as his formal mathematical derivation hadn't been previously published and, I think it is a result which has staggering implications. Prof Rota was a giant in his field and it is amazing to me that his most major contribution seems to have been entirely missed, a historical error I hope to contribute to correcting with your further continued guidance and the collaborative insights of this community.

[Aaron Liu]

Essam Abadir said:

The second scenario—requiring every proof to painstakingly start from foundational logic—defeats the purpose of formalization entirely. Lean’s utility arises precisely from building on well-established theorems and results, enabling practical and concise proofs rather than exhaustive regressions.

I don't understand - what's the point of formalization to you?

[Mario Carneiro]

Essam Abadir said:

I must say though, being new to Lean, it is very counter to my intuition to
not have axioms so I’d love to get a better understanding.

Axioms as normally discussed are the very foundation of formal systems and
any formal argument. To my knowledge you can’t have one without the other,
every proof has them either out in the open or hidden away.

Does Lean syntactically use the word axiom in a different way or is there
something I am misunderstanding understanding about the language?

Lean does use axioms, but all the "acceptable" axioms are for the most part already predefined and available in the library. (There is an additional subtlety that in dependent type theory there is quite a lot which a logician might call an axiom which is instead smuggled in through other schema like inductive types and so does not actually make use of the axiom keyword.)

I believe that your use of axioms to stub out parts of the development you have not investigated and/or wish to take for granted is defensible, but for this use it is clearer to use definitions by sorry instead to make it clear that the definition is not intended to be an opaque self-evident postulate, but rather an "unfinished" part of the proof (even if "unfinished" here means "I have no intention to actually fill this in, but it is in the literature and maybe someone else can fill it in later'). That is, instead of axiom Word : Type, you should use def Word : Type := sorry.

[Aaron Liu]

We have already painstakingly built up a library from foundational logic, that's what mathlib is, and it already contains many well-established results. If you see something missing, you are welcome to add it yourself.

[Mario Carneiro]

Essam Abadir said:

The first scenario—having a complete and sufficient set of axioms—is explicitly ruled out by Gödel’s Incompleteness Theorems, which demonstrate that no consistent, sufficiently rich formal system can prove all truths expressible within it. Thus, expecting Lean, or indeed any formal system, to contain such completeness would seem paradoxical. Furthermore, Russell’s paradox illustrates the risk inherent in naive axiomatics, underscoring why Lean’s axiomatic approach should be valid.

This is not a practical concern. Most theorems of interest are provable outright and do not involve independent statements. These statements do exist, and indeed Lean has some very easy to state independent statements like Nat = Int, but in general they tend to be either non-mathematical questions or very esoteric. If you were to reduce P=NP to an independent statement this would of course also be big news though. There are plenty of ways of dealing with proper axiomatic extensions and independent statements, but I suggest you cross that bridge when you come to it.

[Mario Carneiro]

Attempting to define everything from first principles or redoing well-established proofs such as Shannon's Coding Theorem would only introduce unnecessary error, obfuscation, and complexity into the proof.

On the contrary, redoing a well-established proof will eliminate the unnecessary error caused by potential mis-statement of the theorem. It will certainly add complexity to the proof though. But without these major components, this is but a proof sketch; that's not a bad thing, but we have to recognize it for what it is, and a proof sketch is not a proof (yet) - instead it points the way to the parts that require additional investigation, namely the sorries (or axioms in this case) that remain.

[Mario Carneiro]

Essam Abadir said:

Your critique about my liberal use of axioms is fair and well-taken. My intent, especially as someone new to Lean, was to first outline clearly the theoretical landscape of the proof. Now, guided by your feedback, I'm actively working to convert those axioms which are "new" and further definable (such as Rota's Entropy Theorem) into explicit, verifiable theorems and definitions within Lean’s framework, ideally leveraging established libraries and community-accepted definitions.

This is the right idea. :+1:

I just don't see how the complete absence of axioms is practically achievable (as even Lean’s minimal kernel has axiomatic underpinnings), but definitely do understand the goal is always to minimize assumptions by leveraging formally proven, established results.

Just to be clear, it's not that you can't use axioms, it's that you shouldn't define axioms which are not already in the library. That is, you shouldn't be using the axiom keyword in your project, but it's fine to depend on the prelude library which has a small handful of axioms in it.

[Shreyas Srinivas]

Henrik Böving said:

Shreyas Srinivas said:

(This is false btw, which is my point; you can write false statements like this)

It's not false, just unknown. What is known is that there exists a quadratic reduction of any problem in NL to L (Savitch's theorem) but that does not make them disjoint or equal.

Sorry, some combination of brain misfire and sleep deprivation. I think PSPACE = NPSPACe would have been the accurate version.

[Henrik Böving]

Shreyas Srinivas said:

Henrik Böving said:

Shreyas Srinivas said:

(This is false btw, which is my point; you can write false statements like this)

It's not false, just unknown. What is known is that there exists a quadratic reduction of any problem in NL to L (Savitch's theorem) but that does not make them disjoint or equal.

Sorry, some combination of brain misfire and sleep deprivation. I think PSPACE = NPSPACe would have been the accurate version.

Yes that does follow from Savitch

[Essam Abadir]

Essam Abadir

First, many thanks—especially to Mario—for the steady combination of technical pointers and gentle nudges about community norms.  I come to Lean with a logician’s habit of thinking in terms of axiom systems; the language feels a bit like the trilingual upbringing I grew up with (Arabic ∣ English ∣ French): I can use all three, but still have to stop and ask which tongue I just spoke.  This thread was my way of asking native-Lean speakers how they think in Lean, not merely how to coerce Lean into compiling.

---

What I think I have learned (sanity-check me!)

• Axioms live in their own file(s).

  I have split everything that is still an axiom into a separate ComplexityDefs.lean, as the GitHub repo now shows.

• Be explicit, not “smuggled”.

  Instead of

axiom Word : Type

• the recommended pattern is

def Word : Type := sorry

• That is clearer about intent (“this needs filling in”) and avoids the whiff of hidden postulates.  I confess I would like such lines to sit next to the proof that needs them so reviewers see the dependency chain immediately, but I also appreciate the proof-file clarity Mario’s convention gives.

Let me know if I am mis-reading any of that.

---

The elephant with the big letters

P vs NP

Yes, I put the headline theorem right at the top.  That violates the usual etiquette of “under-promise, over-deliver”, and I did it on purpose.  I wanted maximal scrutiny: if the foundation is sand, better the tower collapses in public.  Please do not read that as naïveté.  The arrows and lemmas will stand or fall with the definitions beneath them, and that is exactly how it should be.

---

On the absence of complexity-theory libraries (@Aaron Liu)

I have pored over mathlib and the various half-started community projects.  As far as I can see there is still no canonical suite of definitions for Machine, timeComplexity, RunsInPolyTime, Cook-Levin, etc.  That is why I keep asking.

Suggesting that a single newcomer “just add the entirety of complexity theory to mathlib” feels a bit like suggesting we re-typeset Principia Mathematica so that the lemma “1 + 1 = 2” is fully formal.  If a result as foundational as Shannon’s Coding Theorem is still missing, I prefer to mark it explicitly as an axiom rather than slide the assumption in under a definition.

---

On the

L ≟ NL

sidebar (@Henrik, @Shreyas)

The log-space discussion is interesting, but it isn’t central to the coding questions nor to the proof sketch itself.  Pointing out that I have not supplied a full formal definition of timeComplexity is a fair observation, yet it circles back to the same practical dilemma: Lean has no ready-made complexity-theory toolkit.  Until that gap is bridged, Mario’s “define-with-sorry, isolate axioms” recipe seems the most honest compromise.

---

Again, thank you all.  Please keep the feedback coming—whether on Lean idioms, on the way I am partitioning axioms vs. definitions, or on any mathematical mis-steps you catch.

[Shreyas Srinivas]

Define with sorry is not a reasonable compromise for the problem you describe. It’s a reasonable starting point provided you have a feasible plan to fill out the sorries. And those sorries still need to be filled out. The whole challenge here is to define these notions of complexity in a theorem prover whose functions are extensionally equal (to be clear there are a few different solutions) . And then to do it in a way that accommodates multiple computational models and nuances. Secondly, and I am sorry that I have to say this, you almost certainly do not have a proof of P != NP. For more details see Scott Aaronson’s blogpost on what a proof of P vs NP should clarify.

[Shreyas Srinivas]

For one thing you need to explain what makes 3SAT so much harder than 2 SAT which has a polynomial time algorithm.

[Shreyas Srinivas]

Oh wait. You claim P = NP. Then I’d like to see this poly time 3SAT algorithm.

[suhr]

Mathlib seem to have some notion of complexity: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/TMComputable.html#Turing.TM2ComputableInTime

No NP class in mathlib yet though.

[Shreyas Srinivas]

Your statements about reductions simply don’t have the right quantifiers. When you reduce problems you have to explain how each input instance is solved via the reduction. Also what on earth is Electrons_On_Circuits_Is_Physical_SAT

[Shreyas Srinivas]

suhr said:

Mathlib seem to have some notion of complexity: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/TMComputable.html#Turing.TM2ComputableInTime

No NP class in mathlib yet though.

This is not super hard to define. The certificate definition should be doable as long as we can express the input encoding to a TM as the concatenation of two input encodings of bounded size

[Shreyas Srinivas]

But let’s take this discussion to a separate thread

[Essam Abadir]

Thanks @suhr that is helpful.

@Mario Carneiro I also found this by searching on your name :) : https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Sat/FromLRAT.lean?utm_source=chatgpt.com

In my definitions file I currently have:

-- Boolean Circuits and SAT
axiom Circuit : Type
instance : Inhabited Circuit := ⟨sorry⟩

axiom encodeCircuit (c : Circuit) : Word
axiom decodeCircuit (w : Word) : Option Circuit
axiom evalCircuit (c : Circuit) (assignment : Word) : Bool

def SAT_problem : Lang :=
  fun w_c => ∃ (c : Circuit) (assignment : Word),
      decodeCircuit w_c = some c ∧ evalCircuit c assignment = true

Using your library could I treat encodeCircuit c as Lean code that produces a CNFFormula; then my SAT_problem can be the predicate ¬ satisfiable φ?

[Essam Abadir]

Shreyas Srinivas said:

suhr said:

Mathlib seem to have some notion of complexity: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/TMComputable.html#Turing.TM2ComputableInTime

No NP class in mathlib yet though.

This is not super hard to define. The certificate definition should be doable as long as we can express the input encoding to a TM as the concatenation of two input encodings of bounded size

Appreciate that @Shreyas Srinivas I'll start a separate thread now on cleaning up the ComplexityDefs.lean file I'm working on.

[Shreyas Srinivas]

My suggestion to start a new thread was to @suhr but you are welcome to do that if you would like to contribute. But I also recommend trying it out in a separate project before making a mathlib PR

[Shreyas Srinivas]

And getting some feedback

[Essam Abadir]

@Shreyas Srinivas In words how would you describe the physical problem that SAT represents in the real world? In Lean, how would you describe it?

I don't think Lean can be used for a constructive proof of P=NP since the constructive algorithm would need to run on a machine that is Turing Complete and, to my knowledge, Lean is not.

The alternative, which Lean is capable of, is a proof of existence ... and I believe Scott Aaronson says he is a fan of those.

[Aaron Liu]

Essam Abadir said:

I don't think Lean can be used for a constructive proof of P=NP since the constructive algorithm would need to run on a machine that is Turing Complete and, to my knowledge, Lean is not.

What reason do you have for believing this?

[Aaron Liu]

Many reductions can be done on a machine that is not turing complete, why do you think P=NP is any different?

[Essam Abadir]

Aaron Liu said:

Essam Abadir said:

I don't think Lean can be used for a constructive proof of P=NP since the constructive algorithm would need to run on a machine that is Turing Complete and, to my knowledge, Lean is not.

What reason do you have for believing this?

My understanding is that Lean programs always terminate and therefore can not . Again, I'm new to the whole environment so please correct me if I'm wrong. Either way, for my particular background (fractal video compression, physics game engines) I'd use a 3GL.

[Aaron Liu]

Why does the constructive algorithm have to run on a turing-complete machine? Why can't it run on a non-turing-complete machine?

[Essam Abadir]

Aaron Liu said:

Why does the constructive algorithm have to run on a turing-complete machine?

The approach of my proof is dependent on Rota's Entropy Theorem (RET) - I fully acknowledge it rises and falls on RET, and, that I'll probably have to port RET to Lean or some equivalent even though the math is 50 years old at this point.

RET shows strict equivalence between physics entropies (Bose-Einstein, Fermi-Dirac, etc.) and Shannon Entropy which strictly implies that physics is computable in polynomial time. The constructive proof would therefore have to run in an environment where anything theoretically computable in computer science (Turing Complete) is computable. I'm sure that regardless what I say in this thread the constructive algorithm will be perceived as some sort of movie. On the other hand, the reason I'm attracted to Lean (or logic more broadly) is that there is a certain certain satisfaction which comes with the proof of existence and Lean allows concrete discussable in this context.

Said differently, a constructive proof would have to be able to compute anything in physics, i.e. your machine must be able compute anything that realizable (or at least compute a physics problem that was thought uncomputable, like Bose-Einstein statistics). This is the basis of Aaronson's Boson Sampling being the problem from which all quantum computing benchmarks derive ... "can you compute what light does using computational automata."

I do have a constructive algorithm which does this, it's off topic for this forum but if you want to check out the constructive proof then see then see this link (https://storage.googleapis.com/daita-assets/sites/egpt/index.html). I have no idea how this could be implemented in Lean and, I think that theorically it is impossible to implement in lean since the automata have to actually run their stochastic processes at large scale. The solution is in the recursive/fractal pattern that the Partition Theory which Rota taught can handle. The constructive algorithm is able to compute wave interference patterns, the double slit (see the interference report showing the expected interference), and Blackbody radiation simulations producing the expected distributions.

As previously discussed in this thread, assuming it is acceptable to take Shannon's Coding Theorem as an axiom (or that the derivation gets added to Lean by me or someone else), my proof will rise and fall on whether Rota's Entropy Theorem holds (assuming that you are willing to accept that SAT is a real world circuit satisfiability problem and not some abstract puzzle).

While related to, but not quite the same as the "can you compute what light does" question, the same combinatoric math enables a fully discrete and digitally computable derivation of Plancks's Law under the assumption of quantum gravity (note, I don't consider the Planck derivation a constructive proof relevant to P=NP but it is a constructive proof of computable physics in the computer science sense of computation: https://www.researchgate.net/publication/387306298_Without_Attraction_You've_Got_Nothing_-_Quantum_Gravity_Derivation_Under_Chaos_Probability_Theories).
(Edited for clarity).

[Mario Carneiro]

Essam Abadir said:

I have pored over mathlib and the various half-started community projects.  As far as I can see there is still no canonical suite of definitions for Machine, timeComplexity, RunsInPolyTime, Cook-Levin, etc.  That is why I keep asking.

Suggesting that a single newcomer “just add the entirety of complexity theory to mathlib” feels a bit like suggesting we re-typeset Principia Mathematica so that the lemma “1 + 1 = 2” is fully formal.  If a result as foundational as Shannon’s Coding Theorem is still missing, I prefer to mark it explicitly as an axiom rather than slide the assumption in under a definition.

The fact is that this project will not be complete until complexity theory is in mathlib, whether that happens because you do it or because others do in the meantime. It's unfortunate, but that's just the way it is when your theorem relies on unformalized prerequisites. You can of course proceed with the project without formalizing complexity theory first, but your claims will be conditional in that case.

There are two main theorems you seem to be relying on here, Shannon's Coding Theorem and Rota's Entropy Theorem. These two are clearly what you should focus most on to make progress. The next step here would be to get a statement, as precise as you can, on which to test peoples' intuitions, because I and many others have strong intuitions that say that P = NP is not provable, so it is probably not necessary to actually go as far as a formal proof to find the "minimal unintuitive lemma" buried in your derivation.

[Mario Carneiro]

A good start would be to determine which of SCT or RET is more likely to be false (or mis-stated / misinterpreted). From your description, I'm inclined to say RET is the suspicious one: Physics is not able to magically solve NP complete problems on its own without a lengthy annealing process in practice, so I suspect something is being idealized incorrectly here.

[Mario Carneiro]

I think the discussion of constructive proofs is mostly a red herring. You can treat Lean as a classical proof system and ignore computability in the metalogic entirely; for a theorem of this form you really want explicit complexity theory and Lean is just as capable of talking about and proving theorems about complexity theory as ZFC. Also keep in mind that P = NP is a statement in complexity theory, not computability theory. It's entirely trivial from a computability perspective, because everything in sight is computable. Lean can solve NP complete problems computably using the brute force algorithm. Similarly, Physics is likely computable but that doesn't mean it is polynomial time.

[Yan Yablonovskiy]

(deleted)

[Johannes Tantow]

On what page is Rotas entropy theorem stated in the book. At the linked page (367) there is no theorem

[Johannes Tantow]

I only skimmed through the book a bit and found nothing that reminds me of computing or any reduction

[Mario Carneiro]

Essam Abadir said:

P vs NP

Yes, I put the headline theorem right at the top.  That violates the usual etiquette of “under-promise, over-deliver”, and I did it on purpose.  I wanted maximal scrutiny: if the foundation is sand, better the tower collapses in public.

By the way, when I said "it will draw extreme skepticism" earlier that was euphemistic for "people will think you are a crank". More skepticism is not always a good thing; if you crank it up too much, rather than getting maximal scrutiny you will get everyone ignoring your work, being dismissive, and/or not assuming you are acting in good faith, which is really not a recipe for productive interaction. I find this a slightly unfortunate aspect of mathematical research work; mathematicians working on a big theorem are known to keep the headline tightly under wraps until they've triple checked everything in order to be able to weather the inevitable storm of skepticism.

[suhr]

As a software developer, I have a somewhat different perspective. I care about two things:

• Whether a person is honest
• Whether a person is willing to work and learn

In the case of this thread, I can believe that OP is honest but I don't see willingness to work: formalizing the statement of the P vs NP problem is within the reach, but OP is unwilling to do it, mentioning Principia Mathematica as an excuse.

I do have a bit of faith in people, so I patiently wait if any work actually will be done.

[Mario Carneiro]

I don't see it so much as unwillingness as a (correct) assessment that it's a lot of work and rather tangential to the purpose of this particular formalization. Clearly they did not sign up to go on a year long yak shaving expedition here, and it's unfortunate that they or someone else needs to in this case.

[suhr]

Is a proper formalization of the statement of a theorem really tangential to the purpose of formalization of a supposed proof of the theorem?

[Essam Abadir]

suhr said:

As a software developer, I have a somewhat different perspective. I care about two things:

• Whether a person is honest
• Whether a person is willing to work and learn

In the case of this thread, I can believe that OP is honest but I don't see willingness to work: formalizing the statement of the P vs NP problem is within the reach, but OP is unwilling to do it, mentioning Principia Mathematica as an excuse.

I do have a bit of faith in people, so I patiently wait if any work actually will be done.

I'll take you at your word and ask that you help since some of this beyond my skills in Lean. For example:

---

As part of formalizing the Rota Entropy Theorem proof sketch I've hit a persistent roadblock in a specific lemma (f_non_decreasing). The core issue seems to stem from proving the positivity (> 0.0) of a Real expression involving Nat coercion, specifically 1 / (↑k + 1), within the context of filtering a list.

Goal:

The high-level goal within the failing lemma is to show filter P (uniformDist (k+1) ++ [0.0]) = uniformDist (k+1), where P is the predicate fun x : Real => decide (x > 0.0). This requires proving intermediate steps, including filter P (uniformDist (k+1)) = uniformDist (k+1). This latter step boils down to proving that for any x in uniformDist (k+1), P x holds. Since x = 1 / (↑k + 1), the specific goal becomes proving 1 / (↑k + 1) > 0.0.

The Problem:

While proving 1 / (↑k + 1) > 0.0 seems straightforward (positive numerator, positive denominator), applying standard tactics and lemmas consistently fails, often with confusing typeclass errors or unification failures.

Attempts Made:

1. Initial Predicate: Started with the predicate (· > 0), relying on Lean's implicit decide, and using tactics like positivity. Ran into issues.
2. Explicit Predicate/Zero: Switched to fun x : Real => decide (x > 0.0) and using the literal 0.0 when adding zero to the list (p' := p ++ [0.0]) to avoid type inference issues between Nat/Int/Real zeros.

3. Proving Denominator Positivity (↑k + 1 > 0.0):

   * norm_cast followed by Nat.succ_pos k: Failed (type mismatch).
   * apply Nat.cast_pos.mpr: Failed because ↑k + 1 doesn't syntactically match ↑n.
   * Rewriting ↑k + 1 to ↑(k+1) using rw [← Nat.cast_add_one k] then apply Nat.cast_pos.mpr: Seemed correct but subsequent steps sometimes failed.
   * Using linarith [Nat.zero_le k]: This seems to work reliably for proving ↑k + 1 > 0.0.

4. Proving Numerator Positivity (1 > 0.0):

   * exact zero_lt_one: Sometimes failed with type mismatches (expecting > 0 vs > 0.0).
   * norm_num: Works reliably.

5. Combining Positivity (div_pos, one_div_pos, inv_pos): After successfully proving h_num_pos : 1 > 0.0 (e.g., with norm_num) and h_den_pos : ↑k + 1 > 0.0 (e.g., with linarith), the final step applying a division positivity rule fails:

   * exact div_pos h_num_pos h_den_pos: Often fails with typeclass instance problem is stuck... PosMulReflectLT ... or similar.
   * apply one_div_pos then exact h_den_pos: Sometimes fails with similar typeclass errors or unification issues.
   * apply inv_pos on (↑k + 1)⁻¹: Similar issues.

It feels like there's a subtle type inference or typeclass resolution issue preventing the final step, even when the prerequisites seem correctly proved.

Minimal Working Example (MWE):

This lemma isolates the failing step:

import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Data.List.Defs -- For List.replicate

open Classical Real List

-- Simplified uniformDist for MWE
noncomputable def uniformDist (n : Nat) : List Real :=
  match n with
  | 0 => []
  | k+1 => replicate (k+1) (1 / (k+1 : Real))

-- The failing lemma attempt
lemma filter_decide_gt_zero_uniformDist_eq_self_MWE {n : Nat} (hn : 0 < n) :
    filter (fun x : Real => decide (x > 0.0)) (uniformDist n) = uniformDist n := by
  apply filter_eq_self.mpr -- Goal: ∀ x ∈ uniformDist n, decide (x > 0.0) = true
  intro x hx_mem
  simp only [uniformDist] at hx_mem
  cases n with
  | zero => exact (Nat.not_lt_zero 0 hn).elim
  | succ k =>
    simp only [mem_replicate] at hx_mem
    obtain ⟨_hnz, hx_eq⟩ := hx_mem
    rw [hx_eq, decide_eq_true_iff] -- Goal: 1 / (↑k + 1) > 0.0

    -- Prove prerequisites seemingly successfully
    have h_num_pos : (1 : Real) > 0.0 := by norm_num
    have h_den_pos : (↑k + 1 : Real) > 0.0 := by
      linarith [Nat.zero_le k] -- linarith seems robust here

    -- This final step often fails with typeclass errors
    exact div_pos h_num_pos h_den_pos
    -- Using apply one_div_pos / exact h_den_pos also tends to fail similarly.

/-
Error Message frequently seen at the `exact div_pos` or `apply one_div_pos` step:
"typeclass instance problem is stuck, it is often due to metavariables
  PosMulReflectLT ?m.XXXX"
(or similar typeclasses related to ordered fields/division rings)
-/

Question:

What is the most robust and correct way to prove 1 / (↑k + 1) > 0.0 in this context, avoiding the typeclass/unification failures we're seeing with div_pos and related lemmas? Is there a different tactic or lemma sequence we should be using?

Thanks for any insights!

---

[Aaron Liu]

positivity seems to work here though?

import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Data.List.Defs

open Classical Real List

-- Simplified uniformDist for MWE
noncomputable def uniformDist (n : Nat) : List Real :=
  match n with
  | 0 => []
  | k+1 => replicate (k+1) (1 / (k+1 : Real))

lemma filter_decide_gt_zero_uniformDist_eq_self_MWE {n : Nat} (hn : 0 < n) :
    filter (fun x : Real => decide (x > 0)) (uniformDist n) = uniformDist n := by
  apply filter_eq_self.mpr
  intro x hx_mem
  simp only [uniformDist] at hx_mem
  cases n with
  | zero => exact (Nat.not_lt_zero 0 hn).elim
  | succ k =>
    simp only [mem_replicate] at hx_mem
    obtain ⟨_hnz, hx_eq⟩ := hx_mem
    rw [hx_eq, decide_eq_true_iff]

    have h_num_pos : (1 : Real) > 0 := by norm_num
    have h_den_pos : (↑k + 1 : Real) > 0 := by
      linarith [Nat.zero_le k]
    positivity

[Mario Carneiro]

:+1: for asking a question which is clearly on topic

[Mario Carneiro]

general recommendation, don't use 0.0 if you want 0. The latter has more lemmas about it and the former should be simped to the same thing

[Mario Carneiro]

(I don't think they are syntactically equal)

[suhr]

Yeah, 0.0 is a Float which is used for programming rather than for math. While there's a coercion of floats into reals, there's not many lemmas about the result of such coercion.

For math you should use 0 instead of 0.0.

[Mario Carneiro]

Not exactly, 0.0 uses an OfScientific instance for the type just like 0 uses OfNat for the type. There is a default instance which uses Float, but this only affects uses where the type cannot be inferred

[suhr]

Yeah, Mathlib implements this in a somewhat roundabout way. You have https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Ring/Unbundled/Rat.html#NNRatCast.toOfScientific, which implements OfScientific for everything that has a canonical homomorphism from rationals.

[Essam Abadir]

Thx that got things a bit further assuming I implemented your advice correctly. I'm very much getting out my depths at this point in terms of understanding what is happening under the hood and the Lean idioms are new to me. In hopes of giving you well structured questions I'm enlisting an LLM to help me write questions up from here:

At the step involving List.filter and are running into trouble with a convert_to step, even after simplifying the setup based on previous advice (thanks @[Forum User Who Provided Positivity Solution]!).

Context:

We are inside a larger proof (f_non_decreasing) and need to prove the following intermediate fact:

-- Goal: Prove that filtering (p ++ [0]) is the same as p
have h_filter_eq_p : p'.filter (fun x : Real => decide (x > 0)) = p := by ...

Where:

• p := uniformDist (k+1) (a list of positive Real numbers 1 / (↑k + 1))
• p' := p ++ [0] (using generic 0, type inferred as Real)
• We have helper lemmas:
  * filter_decide_gt_zero_singleton_zero : filter (fun x : Real => decide (x > 0)) [0] = []
  * filter_decide_gt_zero_uniformDist_eq_self : filter (fun x : Real => decide (x > 0)) (uniformDist n) = uniformDist n (proven using positivity)

The Attempted Proof using convert_to:

have h_filter_eq_p : p'.filter (fun x : Real => decide (x > 0)) = p := by
  simp only [p'] -- Goal: filter (...) (p ++ [0]) = p
  rw [filter_append] -- Goal: filter (...) p ++ filter (...) [0] = p
  -- Use convert_to for robustness against predicate unification issues
  convert_to filter (fun x : Real => decide (x > 0)) p ++ [] = p using 2
  · -- Subgoal 1: prove filter (...) [0] = []
    exact filter_decide_gt_zero_singleton_zero
  -- Main goal after convert: filter (...) p ++ [] = p
  rw [append_nil] -- Goal: filter (...) p = p
  rw [filter_decide_gt_zero_uniformDist_eq_self nk_pos] -- Goal: p = p
  -- rfl -- closes goal

The Problem:

Despite the helper lemmas seeming correct (especially filter_decide_gt_zero_uniformDist_eq_self which now uses positivity successfully), the convert_to step (or sometimes the subsequent rw [filter_decide_gt_zero_uniformDist_eq_self nk_pos]) fails. The typical error is either a type mismatch error involving the predicate (decide (x > 0)) or a failure to unify the goal.

It feels like convert_to isn't simplifying the predicate correctly, or the context within f_non_decreasing is causing issues that weren't present in the isolated MWE for the helper lemma.

Question:

Is convert_to the right approach here? Is there a more robust way to prove h_filter_eq_p given the helper lemmas? Could there be an issue with how the predicate (fun x : Real => decide (x > 0)) is being handled by filter_append vs. convert_to vs. the helper lemmas?

Full Code Context:

import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Data.Rat.Defs
import Mathlib.Data.List.Basic
import PprobablyEqualsNP.PartitionTheoryDefs -- Assuming this file is available

/-! RotaEntropyProof.lean -/

namespace PprobablyEqualsNP.RotaEntropyProof

open Classical Real List PprobablyEqualsNP.PartitionTheoryDefs

-- === Definition of f(n) ===

/-- The function f(n) = H applied to the uniform distribution on n elements. -/
noncomputable def f (H : EntropyFunction) (n : Nat) : Real :=
  if 0 < n then H (uniformDist n) else 0

lemma f_def_alt {H : EntropyFunction} {n : Nat} (hn : 0 < n) : f H n = H (uniformDist n) := by
  rw [f, if_pos hn]

@[simp] lemma length_uniformDist (n : Nat) : length (uniformDist n) = n := by
  cases n <;> simp [uniformDist]

lemma f_one_is_zero {H : EntropyFunction} (hProps : HasEntropyProperties H) : f H 1 = 0 := by
  have h_unif_1 : uniformDist 1 = [1] := by simp [uniformDist]
  rw [f_def_alt]
  · rw [h_unif_1]; exact hProps.prop0
  · exact Nat.zero_lt_one


-- === Helper Lemmas (Using generic 0) ===

-- Define uniformDist here if not in PartitionTheoryDefs or separate file
-- noncomputable def uniformDist (n : Nat) : List Real :=
--   match n with
--   | 0 => []
--   | k+1 => replicate (k+1) (1 / (k+1 : Real))

/-- Helper: filter (fun x : Real => decide (x > 0)) on [0] is []. -/
lemma filter_decide_gt_zero_singleton_zero : filter (fun x : Real => decide (x > 0)) [0] = [] := by
  simp [filter, gt_iff_lt, decide_eq_false_iff_not.mpr (lt_irrefl 0)]

/-- Helper: filter (fun x : Real => decide (x > 0)) on uniformDist n is identity for n > 0. -/
lemma filter_decide_gt_zero_uniformDist_eq_self {n : Nat} (hn : 0 < n) :
    filter (fun x : Real => decide (x > 0)) (uniformDist n) = uniformDist n := by
  apply filter_eq_self.mpr
  intro x hx_mem
  simp only [uniformDist] at hx_mem
  cases n with
  | zero => exact (Nat.not_lt_zero 0 hn).elim
  | succ k =>
    simp only [mem_replicate] at hx_mem
    obtain ⟨_hnz, hx_eq⟩ := hx_mem
    rw [hx_eq, decide_eq_true_iff] -- Goal: 1 / (↑k + 1) > 0
    positivity -- Should solve the goal directly

-- === Main Proof for f_non_decreasing ===

/-- Lemma: f is non-decreasing. Follows from Properties 2 and 5. -/
lemma f_non_decreasing {H : EntropyFunction} (hProps : HasEntropyProperties H) (n : Nat) : f H n ≤ f H (n + 1) := by
  have hn_succ_pos : 0 < n + 1 := Nat.succ_pos n
  rw [f_def_alt hn_succ_pos]
  cases n with
  | zero =>
    simp only [f, dif_neg (Nat.not_lt_zero 0)]
    rw [← f_one_is_zero hProps]
    rfl
  | succ k =>
    have nk_pos : 0 < k + 1 := Nat.succ_pos k
    rw [f_def_alt nk_pos]
    let p := uniformDist (k+1)
    have hp_dist : IsProbDist p := uniformDist_IsProbDist (k+1) nk_pos

    have hp_len_pos : 0 < p.length := by simp [nk_pos]

    let p' := p ++ [0] -- Use generic 0
    have hp'_dist : IsProbDist p' := by
      constructor
      · intro pi hpi_mem; rw [mem_append] at hpi_mem
        cases hpi_mem with | inl hp => exact hp_dist.1 pi hp | inr h0 => rw [mem_singleton.mp h0]; norm_num -- 0 ≥ 0
      · rw [sum_append, sum_singleton, hp_dist.2]; norm_num -- 1 + 0 = 1

    have hp'_len_val : p'.length = k + 2 := by simp
    have hp'_len_pos : 0 < p'.length := by rw [hp'_len_val]; positivity

    -- Apply Prop 5
    have h_p'_le_unif : H p' ≤ H (uniformDist p'.length) :=
      hProps.prop5 p' hp'_dist hp'_len_pos
    rw [hp'_len_val] at h_p'_le_unif

    -- Apply Prop 2 - Ensure predicate matches EXACTLY
    have h_p'_eq_filter : H p' = H (p'.filter (fun x : Real => decide (x > 0))) := Eq.symm (hProps.prop2 p' hp'_dist)

    -- Show filter p' (>0) = p using helper lemmas
    have h_filter_eq_p : p'.filter (fun x : Real => decide (x > 0)) = p := by
      simp only [p'] -- Goal: filter (...) (p ++ [0]) = p
      rw [filter_append] -- Goal: filter (...) p ++ filter (...) [0] = p
      -- Use convert_to for robustness
      convert_to filter (fun x : Real => decide (x > 0)) p ++ [] = p using 2
      · exact filter_decide_gt_zero_singleton_zero -- Prove filter (...) [0] = []
      rw [append_nil] -- Goal: filter (...) p = p
      rw [filter_decide_gt_zero_uniformDist_eq_self nk_pos] -- Goal: p = p

    -- Combine
    have h_p'_eq_Hp : H p' = H p := by simp [h_p'_eq_filter, h_filter_eq_p]
    rw [h_p'_eq_Hp] at h_p'_le_unif
    exact h_p'_le_unif

-- ....
end PprobablyEqualsNP.RotaEntropyProof

[Mario Carneiro]

In hopes of giving you well structured questions I'm enlisting an LLM to help me write questions up from here

I don't think this is necessary. The actual context you need to provide along with questions (e.g. code blocks) should be written by you alone, and the grammar around that does not need to be polished (and LLMs tend to generate unnecessarily long posts with low signal to noise ratio). Unless you have serious difficulties writing in english I would suggest just asking questions au naturel

[Mario Carneiro]

in particular, when something is wrong, it can be difficult to tell the difference between your mistake and the LLM's mistake

[Mario Carneiro]

There is an instance of this in your post:

import PprobablyEqualsNP.PartitionTheoryDefs -- Assuming this file is available

This makes the code example not an MWE. Is this line written by you or hallucinated?

[Michael Rothgang]

To add to this: recently, there have been a number of low-effort questions asked --- where somebody would (seemingly) copy-paste LLM output without understanding or thinking about it. This makes a number of people rather cautious with LLM-written posts and reconsider responding. If you write in your own words, you avoid this trap.

[Essam Abadir]

Johannes Tantow said:

On what page is Rotas entropy theorem stated in the book. At the linked page (367) there is no theorem

Rota's Entropy Theorem doesn't actually have a name in the book - I gave it that moniker in lieu of the following: Most of Chapter 7 constitutes a proof culminating on p. 382 that any function displaying the 5 properties Rota describes is an entropy function which is mathematically equivalent to scaled Shannon Entropy. The preceding chapters 1-6 show that all the "interesting distributions" of nature have those properties. p. 383 gives the computability consequence since in Information Theory, Shannon's Coding Theorem gives the computability of any function displaying Shannon Entropy - as explained by Rota, Shannon's Coding Theorem demands that there is a yes/no series of questions (which can be encoded in boolean gates) that give an O(n log n) encoding, but, as also explained by Rota, finding that encoding can be "highly non-trivial."

[Mario Carneiro]

Here's a better MWE:

import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Data.Rat.Defs
import Mathlib.Data.List.Basic

open Real List

-- Simplified uniformDist for MWE
noncomputable def uniformDist (n : Nat) : List Real :=
  match n with
  | 0 => []
  | k+1 => replicate (k+1) (1 / (k+1 : Real))

@[simp] lemma length_uniformDist (n : Nat) : length (uniformDist n) = n := by
  cases n <;> simp [uniformDist]

/-- Helper: filter (fun x : Real => decide (x > 0)) on [0] is []. -/
lemma filter_decide_gt_zero_singleton_zero : filter (fun x : Real => decide (x > 0)) [0] = [] := by
  simp [filter, gt_iff_lt, decide_eq_false_iff_not.mpr (lt_irrefl 0)]

/-- Helper: filter (fun x : Real => decide (x > 0)) on uniformDist n is identity for n > 0. -/
lemma filter_decide_gt_zero_uniformDist_eq_self {n : Nat} (hn : 0 < n) :
    filter (fun x : Real => decide (x > 0)) (uniformDist n) = uniformDist n := by
  apply filter_eq_self.mpr
  intro x hx_mem
  simp only [uniformDist] at hx_mem
  cases n with
  | zero => exact (Nat.not_lt_zero 0 hn).elim
  | succ k =>
    simp only [mem_replicate] at hx_mem
    obtain ⟨_hnz, hx_eq⟩ := hx_mem
    rw [hx_eq, decide_eq_true_iff] -- Goal: 1 / (↑k + 1) > 0
    positivity -- Should solve the goal directly

-- === Main Proof for f_non_decreasing ===

/-- Lemma: f is non-decreasing. Follows from Properties 2 and 5. -/
lemma f_non_decreasing (k : Nat) : True := by
  have nk_pos : 0 < k + 1 := Nat.succ_pos k
  let p := uniformDist (k+1)
  have hp_len_pos : 0 < p.length := sorry

  let p' := p ++ [0] -- Use generic 0
  have hp'_len_val : p'.length = k + 2 := sorry
  have hp'_len_pos : 0 < p'.length := by rw [hp'_len_val]; positivity

  suffices p'.filter (fun x : Real => decide (x > 0)) = p by trivial

  simp only [p'] -- Goal: filter (...) (p ++ [0]) = p
  rw [filter_append] -- Goal: filter (...) p ++ filter (...) [0] = p
  -- Use convert_to for robustness
  convert_to filter (fun x : Real => decide (x > 0)) p ++ [] = p using 2
  · exact filter_decide_gt_zero_singleton_zero -- Prove filter (...) [0] = []
  rw [append_nil] -- Goal: filter (...) p = p
  rw [filter_decide_gt_zero_uniformDist_eq_self nk_pos] -- Goal: p = p

[Mario Carneiro]

and here's a proof of the main goal:

  suffices p'.filter (fun x : Real => decide (x > 0)) = p by trivial

  simp [p', p, filter_append, uniformDist]
  linarith

[Essam Abadir]

Mario Carneiro said:

There is an instance of this in your post:

import PprobablyEqualsNP.PartitionTheoryDefs -- Assuming this file is available

This makes the code example not an MWE. Is this line written by you or hallucinated?

I added that line since I didn't post the file.

I understand, was aiming for transparency. Hopefully at this point in the thread it's not taken as a low effort post.

[Mario Carneiro]

Note that I removed an open Classical, which is likely causing problems because it is changing the decision procedure used in the filter

[Mario Carneiro]

You should remove references to your project when constructing a #mwe

[Mario Carneiro]

either by inlining everything, or by sorrying everything that is not directly relevant to the question. In the MWE I posted, you will notice that I removed everything to do with EntropyFunction since it's not relevant, and so all the dependencies on the other file went away

[Essam Abadir]

Mario Carneiro said:

Note that I removed an open Classical, which is likely causing problems because it is changing the decision procedure used in the filter

THANK YOU! I'll pipe this back in and try to digest the Lean idioms a bit more. You've saved me a few weeks at least on my Yak shaving adventure.

[Mario Carneiro]

fun fact, I noticed this because mathlib has a linter which warns whenever you open Classical

[Mario Carneiro]

because you aren't the only one to be bitten by this

[Essam Abadir]

Mario Carneiro said:

fun fact, I noticed this because mathlib has a linter which warns whenever you open Classical

I would have been trying to find that forever.