solvlabs.co , Savelii K.

"[The history of] mathematics is, to a large extent, invention of better notations" - Feynman Lectures on Physics

Purely illustrative example: if two groups of cells from different biological conditions but processed in the same batch show distinct gene expression signatures, then they represent different cell types or states.

-- Import required libraries. In a real-world case, you may need to import or define 
-- additional mathematical structures.
import data.real.basic

-- Define axioms
axiom CellIndependence (Cell : Type) : Prop
axiom GeneExpression (Cell : Type) : Cell → ℝ
axiom NoiseModelable : Prop
axiom UniqueSignature (CellType : Type) : Prop
axiom BatchEffect : Prop

-- Define your theorem
theorem DifferentSignaturesImplyDifferentTypes
  (Cell : Type) (C1 C2 : set Cell) (Condition1 Condition2 : Prop)
  (SameBatch : Prop) : Prop :=
begin
  -- Here something like Magnushammer or ReProver 
	-- would attempt to perform a formal proof.
  sorry
end

Some further exploration:

<aside> 👩‍🔬 is there isomorphism between methematics and programming?

</aside>

Yes, there are isomorphisms between certain aspects of mathematics and programming. For example, category theory in mathematics has correspondences with functional programming concepts like functors and monads. Lambda calculus serves as a foundation for functional programming languages. Boolean algebra is directly applicable in digital circuit design and programming logic. However, the two disciplines are not completely isomorphic; they have different goals and methodologies.

<aside> 👩‍🔬 how does it relate to Lean?

</aside>

Lean is a theorem prover and programming language designed to formalize mathematical proofs. It provides a platform where the isomorphisms between mathematics and programming are explicitly realized. It uses a dependent type theory as its logical foundation, incorporating elements from both mathematics (like set theory and formal logic) and computer science (like type theory).

In Lean, mathematical objects and theorems are represented in a formal language, and proofs can be constructed interactively. These proofs are verified by the Lean kernel, ensuring they are logically sound. This connects to the "program as proof" paradigm seen in languages based on the Curry-Howard isomorphism, which establishes a correspondence between computer programs and mathematical proofs.

So, Lean is a direct example of how concepts in mathematics and programming can be mapped onto each other.

<aside> 👩‍🔬 how Lean is different from Isabelle and Coq

</aside>

Lean, Isabelle, and Coq are all interactive theorem provers, but they differ in their logical foundations, design philosophies, and feature sets. Here's a quick rundown:

1. Logical Foundation:
   • Lean: Dependent type theory, similar to Coq.
   • Isabelle: Uses higher-order logic (HOL) and also supports Zermelo-Fraenkel set theory.
   • Coq: Also based on dependent type theory (Calculus of Inductive Constructions).
2. User Experience and Ecosystem:
   • Lean: Aims for a more user-friendly experience; strong focus on automation and usability.
   • Isabelle: Known for its powerful Isar proof language and extensive libraries.
   • Coq: Has a steep learning curve but is powerful; extensive libraries and plugins.
3. Automation:
   • Lean: Built-in automation tactics are more limited but growing; relies on the mathlib library for additional support.
   • Isabelle: Sledgehammer tool can automatically find proofs using ATPs (Automated Theorem Provers).
   • Coq: Well-established tactics and plugins for automation, like Ltac.
4. Community and Application:
   • Lean: Newer and has a smaller community; however, it's increasingly being adopted for formalizing mathematics.
   • Isabelle: Broadly used in academia and industry for formal verification.
   • Coq: Widely used for both formal mathematics and software verification.
5. Interoperability and Code Extraction:
   • Lean: Has fewer options for code extraction compared to Coq.
   • Isabelle: Allows code extraction to functional languages like Haskell and ML.
   • Coq: Supports code extraction to languages like Haskell, OCaml, and Scheme.

Each has its own strengths and weaknesses, and the best choice often depends on the specific requirements of a project.