القائمة
Prove statements by assuming the negation and deriving a contradiction. Triggers on "cannot exist", "impossible", "no such", "prove X is irrational", "infinitely many", "there is no"
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
استنادا إلى تصنيف SOC المهني
Explore a mathematical conjecture - gather evidence, find counterexamples, or build toward a proof. Triggers on "explore", "investigate", "what if", "is it true that", "find pattern", "check if"
Determine convergence or divergence of series using ratio test, root test, comparison test, and integral test. Triggers on "series converges", "test for convergence", "ratio test", "root test", "comparison test", "integral test", "sum of 1/n"
Prove geometric theorems using coordinate geometry. Convert shapes to algebraic expressions, use distance formula, midpoint formula, and slope calculations. Triggers on "prove using coordinates", "analytic geometry", "distance formula", "show collinear", "prove perpendicular", "prove parallel"
Prove identities or existence using combinatorial counting - double counting, bijections, inclusion-exclusion. Triggers on "count", "number of ways", "how many", "bijection", "one-to-one correspondence", "combinatorial proof"
Prove statements directly by assuming the hypothesis and deriving the conclusion through logical steps. Triggers on "prove directly", "show that", "demonstrate", "verify", "simple proof"
Prove limit statements using epsilon-delta definitions. Triggers on "epsilon-delta", "limit", "prove continuous", "show limit equals", "formal limit proof"
| name | proof-by-contradiction |
| description | Prove statements by assuming the negation and deriving a contradiction. Triggers on "cannot exist", "impossible", "no such", "prove X is irrational", "infinitely many", "there is no" |
Prove P by assuming ¬P and deriving a contradiction.
| Original | Negation |
|---|---|
| √2 is irrational | √2 = p/q for integers p,q |
| Infinitely many primes | Finitely many primes: {p₁,...,pₙ} |
| No X exists | Some X exists |
symbolic_compute: Help formalize the negationFrom ¬P, derive properties:
Common contradiction patterns:
theorem statement : P := by
by_contra h -- h : ¬P
-- derive contradiction
-- ...
exact absurd fact1 fact2
-- or: contradiction
Key tactics:
by_contra h - assume negationpush_neg at h - simplify negated statementabsurd - derive False from P and ¬Pcontradiction - automatic contradiction finderexfalso - switch to proving False**Theorem:** [Statement]
**Proof by contradiction:**
Assume for contradiction that [¬P].
Then [consequence 1].
And [consequence 2].
But this means [contradiction], which is impossible.
Therefore, [P] must be true. ∎
**Lean proof:**
[Full code with comments]
Irrationality of √2:
Infinitude of primes: