Prove2Me

lean_workbook_plus_8045

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

We can also use conditional probability: We want to find the value of P(genetically modified∣sprouts)P(\text{genetically modified}|\text{sprouts}). We know this is equal to P(genetically modified and sprouts)P(sprouts)\frac{P(\text{genetically modified and sprouts})}{P(\text{sprouts})} which in turn is 25⋅1225⋅12+35⋅13\frac{\frac{2}{5}\cdot\frac{1}{2}}{\frac{2}{5}\cdot\frac{1}{2}+\frac{3}{5}\cdot\frac{1}{3}}, or simply 12\boxed{\frac{1}{2}}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8045  (p q r s : ℝ)
  (h₀ : p = 2 / 5)
  (h₁ : q = 1 / 2)
  (h₂ : r = 3 / 5)
  (h₃ : s = 1 / 3)
  (h₄ : p * q = r * s) :
  p * q / (p * q + r * s) = 1 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph