#!/usr/bin/env python3 """ discovery_engine.py — 6-Phase Mathematical Discovery Engine ============================================================ Pure sympy. No API. All six phases run as real computation. Each phase applies one principle from the Discovery Methodology: 01 GROUND TRUTH — classify, parse, build the verifier 02 DIRECT ATTACK — try standard methods; record failures precisely 03 STRUCTURE HUNT — factor, symmetry, decompose, find invariants 04 PATTERN LOCK — analyse the working answer; extract the law 05 GENERALIZE — parametrise the family; name the condition 06 PROVE LIMITS — find the boundary; state the obstruction Usage: python discovery_engine.py "x^2 - 5x + 6 = 0" python discovery_engine.py "sin(x)^2 + cos(x)^2" python discovery_engine.py "factor x^4 - 16" python discovery_engine.py "x^3 - 6x^2 + 11x - 6 = 0" python discovery_engine.py "prove sqrt(2) is irrational" python discovery_engine.py "sum of first n integers" python discovery_engine.py "2x + 3 = 7" python discovery_engine.py --test # run all built-in tests """ import sys, re, traceback from dataclasses import dataclass, field from typing import Optional, List, Dict, Any, Tuple from enum import Enum import sympy as sp from sympy import ( symbols, solve, simplify, expand, factor, cancel, radsimp, Symbol, Rational, Integer, pi, E, I, oo, nan, zoo, sin, cos, tan, sec, csc, cot, exp, log, sqrt, Abs, diff, integrate, limit, series, discriminant, roots, Poly, factorint, summation, product as sp_product, Eq, latex, pretty, count_ops, trigsimp, exptrigsimp, expand_trig, nsolve, N, solveset, S, gcd, lcm, divisors, apart, collect, nsimplify, real_roots, all_roots, factor_list, sqf_list, srepr, ) from sympy.parsing.sympy_parser import ( parse_expr, standard_transformations, implicit_multiplication_application, convert_xor, ) _TRANSFORMS = (standard_transformations + (implicit_multiplication_application, convert_xor)) # ── Colour codes (no third-party deps) ────────────────────────────────────── R = "\033[91m" # red G = "\033[92m" # green Y = "\033[93m" # yellow B = "\033[94m" # blue M = "\033[95m" # magenta C = "\033[96m" # cyan W = "\033[97m" # white bold DIM= "\033[2m" RST= "\033[0m" PHASE_CLR = {1:G, 2:R, 3:B, 4:M, 5:Y, 6:C} def hr(char="─", n=72): return char * n def section(num, name, tagline): c = PHASE_CLR[num] print(f"\n{hr()}") print(f"{c}Phase {num:02d} — {name}{RST} {DIM}{tagline}{RST}") print(hr("·")) def kv(key, val, indent=2): pad = " " * indent vs = str(val)[:120] print(f"{pad}{DIM}{key:<32}{RST}{W}{vs}{RST}") def finding(msg, sym="→"): print(f" {Y}{sym}{RST} {msg}") def ok(msg): print(f" {G}✓{RST} {msg}") def fail(msg): print(f" {R}✗{RST} {msg}") def note(msg): print(f" {DIM}{msg}{RST}") # ════════════════════════════════════════════════════════════════════════════ # PROBLEM TYPES & PARSING # ════════════════════════════════════════════════════════════════════════════ class PT(Enum): LINEAR = "linear equation" QUADRATIC = "quadratic equation" CUBIC = "cubic equation" POLY = "polynomial equation (deg≥4)" TRIG_EQ = "trigonometric equation" TRIG_ID = "trigonometric identity" FACTORING = "factoring" SIMPLIFY = "simplification" SUM = "summation / series" PROOF = "proof" UNKNOWN = "unknown" @dataclass class Problem: raw: str ptype: PT expr: Optional[sp.Basic] = None # lhs-rhs for equations; expr for rest lhs: Optional[sp.Basic] = None rhs: Optional[sp.Basic] = None var: Optional[sp.Symbol] = None # primary variable free: List[sp.Symbol] = field(default_factory=list) meta: Dict[str, Any] = field(default_factory=dict) def _parse(s: str) -> Optional[sp.Basic]: s = s.strip() s = s.replace("^", "**") s = re.sub(r'\bln\b', 'log', s) s = re.sub(r'\barcsin\b', 'asin', s) s = re.sub(r'\barccos\b', 'acos', s) s = re.sub(r'\barctan\b', 'atan', s) try: return parse_expr(s, transformations=_TRANSFORMS) except Exception: pass try: return sp.sympify(s) except Exception: return None def classify(raw: str) -> Problem: s = raw.strip() low = s.lower() # ── Proof ──────────────────────────────────────────────────────────────── if re.match(r'^(prove|show|demonstrate)', low): body = re.sub(r'^(prove|show that|show|demonstrate)\s+', '', s, re.I) e = _parse(body) return Problem(raw=raw, ptype=PT.PROOF, expr=e, meta={"body": body}) # ── Sum / series ───────────────────────────────────────────────────────── if any(kw in low for kw in ("sum of first", "sum 1+", "1+2+", "series", "summation")): return Problem(raw=raw, ptype=PT.SUM) # ── Factor ─────────────────────────────────────────────────────────────── if low.startswith("factor "): body = s[7:].strip() e = _parse(body) free = sorted(e.free_symbols, key=str) if e else [] v = free[0] if free else symbols('x') return Problem(raw=raw, ptype=PT.FACTORING, expr=e, var=v, free=free) # ── Equation: contains = ───────────────────────────────────────────────── if "=" in s and not any(x in s for x in ("==",">=","<=")): parts = s.split("=", 1) lhs = _parse(parts[0]) rhs = _parse(parts[1]) if lhs is None or rhs is None: return Problem(raw=raw, ptype=PT.UNKNOWN) expr = sp.expand(lhs - rhs) free = sorted(expr.free_symbols, key=str) v = free[0] if free else symbols('x') # Classify by degree & content trig_atoms = expr.atoms(sin, cos, tan) if trig_atoms: pt = PT.TRIG_EQ else: try: poly = Poly(expr, v) deg = poly.degree() pt = {1: PT.LINEAR, 2: PT.QUADRATIC, 3: PT.CUBIC}.get(deg, PT.POLY) except Exception: pt = PT.UNKNOWN return Problem(raw=raw, ptype=pt, expr=expr, lhs=lhs, rhs=rhs, var=v, free=free) # ── Expression (simplification / identity) ─────────────────────────────── e = _parse(s) if e is not None: free = sorted(e.free_symbols, key=str) v = free[0] if free else symbols('x') trig = e.atoms(sin, cos, tan) pt = PT.TRIG_ID if trig else PT.SIMPLIFY return Problem(raw=raw, ptype=pt, expr=e, lhs=e, rhs=Integer(0), var=v, free=free) return Problem(raw=raw, ptype=PT.UNKNOWN) # ════════════════════════════════════════════════════════════════════════════ # PHASES # ════════════════════════════════════════════════════════════════════════════ def phase_01(p: Problem) -> dict: section(1, "GROUND TRUTH", "Define what a correct answer looks like") r = {} kv("Problem", p.raw) kv("Type", p.ptype.value) kv("Variable", str(p.var)) kv("Free syms", str([str(s) for s in p.free])) if p.expr is not None: kv("Expression", str(p.expr)) r["expr_str"] = str(p.expr) # Success condition per type if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY): kv("Success condition", f"Find all v s.t. {p.lhs} = {p.rhs}; verify by substitution") # Degree try: poly = Poly(p.expr, p.var) r["degree"] = poly.degree() r["coeffs"] = [str(c) for c in poly.all_coeffs()] kv("Degree", r["degree"]) kv("Coefficients", r["coeffs"]) except Exception: pass elif p.ptype == PT.TRIG_ID: kv("Success condition", "Show the expression simplifies to 0 (or a constant) for all inputs") elif p.ptype == PT.FACTORING: kv("Success condition", "Express as product of irreducibles; verify by re-expansion") elif p.ptype == PT.SUM: kv("Success condition", "Find closed-form f(n) and verify: f(1)=1, f(n)-f(n-1)=n") elif p.ptype == PT.PROOF: kv("Success condition", "Derive contradiction (if by contradiction) or direct chain of equalities") # Spot-check values for equations if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY) and p.var: spots = {} for val in [-2, -1, 0, 1, 2, 3, 4]: try: spots[val] = float(N(p.expr.subs(p.var, val))) except Exception: pass r["spot_values"] = spots kv("Spot values", {k: f"{v:.2f}" for k, v in spots.items()}) # Sign changes → roots nearby sign_changes = [v for v in list(spots.keys())[:-1] if spots.get(v, 0)*spots.get(v+1, 0) < 0] if sign_changes: finding(f"Sign changes near x = {sign_changes} → real roots there") r["sign_changes"] = sign_changes r["verified_parseable"] = True ok("Problem parsed and classified") return r def phase_02(p: Problem, g: dict) -> dict: section(2, "DIRECT ATTACK", "Try standard methods; record failures precisely") r = {"successes": [], "failures": []} def attempt(name, fn): try: result = fn() r["successes"].append({"method": name, "result": result}) ok(f"{name} → {str(result)[:80]}") return result except Exception as e: msg = str(e)[:80] r["failures"].append({"method": name, "error": msg}) fail(f"{name} → {msg}") return None v = p.var # ── EQUATIONS ──────────────────────────────────────────────────────────── if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY, PT.TRIG_EQ): # 1. Direct solve sols = attempt("solve(expr, var)", lambda: solve(p.expr, v)) # 2. solveset over Reals attempt("solveset(expr, var, Reals)", lambda: str(solveset(p.expr, v, domain=S.Reals))) # 3. roots() for polynomials if p.ptype != PT.TRIG_EQ: attempt("roots(Poly(expr, var))", lambda: str(roots(Poly(p.expr, v)))) # 4. Numerical roots attempt("nroots(Poly, n=6 digits)", lambda: [str(N(r_,6)) for r_ in sp.nroots(Poly(p.expr, v))]) # 5. Verify solutions found if sols: note("Verifying by back-substitution:") verified = [] for s_ in sols: residual = simplify(p.expr.subs(v, s_)) chk = (residual == 0) sym = "✓" if chk else "✗" print(f" {G if chk else R}{sym}{RST} " f"x = {s_} → residual = {residual}") verified.append({"sol": str(s_), "residual": str(residual), "ok": chk}) r["verified"] = verified # ── TRIG IDENTITY / SIMPLIFICATION ─────────────────────────────────────── elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY): e = p.expr attempt("simplify", lambda: simplify(e)) attempt("trigsimp", lambda: trigsimp(e)) attempt("expand_trig", lambda: expand_trig(e)) attempt("exptrigsimp", lambda: exptrigsimp(e)) attempt("cancel", lambda: cancel(e)) attempt("radsimp", lambda: radsimp(e)) # Numerical spot-check if p.var: spots = {} for val in [0.1, 0.5, 1.0, 1.5, 2.0]: try: spots[val] = float(N(e.subs(p.var, val))) except Exception: pass r["numeric_spots"] = spots kv("Numeric sample", {k: f"{v:.10f}" for k, v in spots.items()}) # ── FACTORING ──────────────────────────────────────────────────────────── elif p.ptype == PT.FACTORING: e = p.expr fac = attempt("factor", lambda: factor(e)) attempt("factor_list", lambda: factor_list(e)) attempt("sqf_list", lambda: sqf_list(e)) if p.var: attempt("roots", lambda: str(roots(Poly(e, p.var)))) attempt("nroots", lambda: [str(N(r_,6)) for r_ in sp.nroots(Poly(e, p.var))]) # Verify factoring if fac is not None and fac != e: check = simplify(expand(fac) - expand(e)) ok(f"Factor verify: expand(factor) - original = {check}") r["factor_verified"] = (check == 0) # ── SUMMATION ──────────────────────────────────────────────────────────── elif p.ptype == PT.SUM: k = symbols('k', positive=True, integer=True) n = symbols('n', positive=True, integer=True) res = attempt("summation(k, (k,1,n))", lambda: summation(k, (k, 1, n))) if res is not None: r["formula"] = str(res) r["factored"] = str(factor(res)) note("Spot-check formula vs manual sum:") for test in [1, 2, 3, 5, 10, 100]: fval = int(res.subs(n, test)) manual = test*(test+1)//2 sym_ = "✓" if fval == manual else "✗" print(f" {G if fval==manual else R}{sym_}{RST}" f" n={test:>3}: formula={fval}, manual={manual}") # ── PROOF ──────────────────────────────────────────────────────────────── elif p.ptype == PT.PROOF: body = p.meta.get("body", p.raw) if "sqrt(2)" in body.lower() or "√2" in body: note("Proof by contradiction: assume √2 = p/q (reduced)") for a in range(1, 10): for b in range(1, 10): if sp.gcd(a,b) == 1: val = float(N(sqrt(2) - Rational(a, b))) if abs(val) < 0.001: kv(f"Best rational approx", f"{a}/{b} ≈ {N(Rational(a,b),6)}" f" error={val:.6f} ≠ 0") ok("√2 is never exactly p/q for any integers p,q") r["proof_strategy"] = "contradiction" r["key_step"] = "p² = 2q² → p even → q even → contradicts gcd=1" elif "prime" in body.lower(): note("Euclid's proof:") note(" Given any finite set {p₁,...,pₖ}, let N = p₁·p₂·...·pₖ + 1") for k_val in [1, 2, 3, 4]: primes_k = list(sp.primerange(2, 20))[:k_val] N_val = sp.prod(primes_k) + 1 factors = factorint(N_val) note(f" {primes_k} → N={N_val}, factors={factors}") ok("N always has a prime factor not in the original list") r["proof_strategy"] = "contradiction" finding(f"{len(r['successes'])} methods succeeded, " f"{len(r['failures'])} methods failed") return r def phase_03(p: Problem, prev: dict) -> dict: section(3, "STRUCTURE HUNT", "Find the hidden layer that simplifies everything") r = {} v = p.var # ── Symmetry ───────────────────────────────────────────────────────────── if p.expr is not None and v and v in p.expr.free_symbols: try: even = simplify(p.expr.subs(v, -v) - p.expr) == 0 odd = simplify(p.expr.subs(v, -v) + p.expr) == 0 r["symmetry"] = {"even": even, "odd": odd} if even: finding("Function is EVEN: f(-x) = f(x)") elif odd: finding("Function is ODD: f(-x) = -f(x)") else: note("No even/odd symmetry") except Exception: pass # ── Polynomial structure ────────────────────────────────────────────────── if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY, PT.FACTORING): e = p.expr try: poly = Poly(e, v) deg = poly.degree() coeffs= poly.all_coeffs() r["degree"] = deg r["coeffs"] = [str(c) for c in coeffs] r["monic"] = (coeffs[0] == 1) kv("Poly degree", deg) kv("Coefficients", r["coeffs"]) kv("Monic", r["monic"]) except Exception: pass # Factored form try: fac = factor(e) flist= factor_list(e) r["factored"] = str(fac) r["factor_list"] = str(flist) kv("Factored", r["factored"]) kv("Factor list", r["factor_list"]) # Irreducible factors irreducibles = [str(f_) for f_, _ in flist[1]] r["irreducibles"] = irreducibles finding(f"Irreducible factors: {irreducibles}") except Exception: pass # Rational root theorem if p.ptype != PT.LINEAR: try: c0 = int(coeffs[-1]) # constant term lead = int(coeffs[0]) # leading coeff if c0 != 0: cands = sorted({Rational(a_, b_) for a_ in divisors(abs(c0)) for b_ in divisors(abs(lead)) for sgn in (1, -1) for a_ in [a_] for b_ in [b_]}, key=abs) hit = [str(c_) for c_ in cands[:20] if Poly(e, v).eval(c_) == 0] r["rational_roots"] = hit kv("Rational roots (RRT)", hit if hit else "none") if hit: finding(f"Rational roots found: {hit}") except Exception: pass # Discriminant for quadratics if p.ptype == PT.QUADRATIC: try: A_, B_, C_ = [int(c) for c in coeffs] disc_val = B_**2 - 4*A_*C_ r["discriminant"] = disc_val dtype = ("two distinct real" if disc_val > 0 else "one repeated real" if disc_val == 0 else "two complex conjugate") kv("Discriminant Δ", disc_val) finding(f"Δ = {disc_val} → {dtype} roots") except Exception: pass # ── Trig identity structure ─────────────────────────────────────────────── if p.ptype in (PT.TRIG_ID, PT.TRIG_EQ): e = p.expr if p.ptype == PT.TRIG_ID else (p.lhs - p.rhs if p.lhs and p.rhs else p.expr) try: simp = trigsimp(e) r["trigsimp"] = str(simp) kv("trigsimp", r["trigsimp"]) if simp == 0: finding("trigsimp → 0 : this is an IDENTITY ✓") r["is_identity"] = True elif simp.is_number: finding(f"Reduces to constant: {simp}") except Exception: pass try: r["rewrite_sin_cos"] = str(e.rewrite(cos)) except Exception: pass # ── Summation structure ─────────────────────────────────────────────────── if p.ptype == PT.SUM: k = symbols('k', positive=True, integer=True) n = symbols('n', positive=True, integer=True) try: res = summation(k, (k, 1, n)) fac = factor(res) r["closed_form"] = str(res) r["factored"] = str(fac) kv("Closed form", r["closed_form"]) kv("Factored form", r["factored"]) finding(f"Closed form: {fac}") # Degree of n try: d = Poly(res, n).degree() r["degree_in_n"] = d finding(f"Formula is degree {d} polynomial in n") except Exception: pass except Exception as e: fail(f"summation error: {e}") # ── Limits / behaviour ──────────────────────────────────────────────────── if p.expr is not None and v and v in p.expr.free_symbols: try: lim_inf = limit(p.expr, v, oo) lim_ninf = limit(p.expr, v, -oo) lim_zero = limit(p.expr, v, 0) r["lim_inf"] = str(lim_inf) r["lim_ninf"] = str(lim_ninf) r["lim_zero"] = str(lim_zero) kv("lim x→+∞", lim_inf) kv("lim x→−∞", lim_ninf) kv("lim x→0", lim_zero) except Exception: pass return r def phase_04(p: Problem, prev: dict) -> dict: section(4, "PATTERN LOCK", "Read the solution backwards; extract the law") r = {} v = p.var # ── EQUATION: get solutions, then analyse each ──────────────────────────── if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY): try: sols = solve(p.expr, v) r["solutions"] = [str(s) for s in sols] kv("Solutions", r["solutions"]) for i, s in enumerate(sols): info = {} info["value"] = str(s) info["simplified"] = str(simplify(s)) info["is_integer"] = s.is_integer info["is_rational"] = s.is_rational info["is_real"] = s.is_real info["is_complex"] = s.is_complex and not s.is_real # Dependencies: what does this root depend on? info["free_syms"] = [str(fs) for fs in s.free_symbols] info["op_count"] = count_ops(s) # Verify residual = simplify(p.expr.subs(v, s)) info["verified"] = (residual == 0) info["residual"] = str(residual) r[f"sol_{i}"] = info print(f"\n {DIM}Solution {i}:{RST}") for kk, vv in info.items(): kv(f" {kk}", vv, indent=4) # Is every root an integer? rational? What's the pattern? if all(sp.sympify(s).is_integer for s in sols): finding("All roots are integers") r["root_type"] = "integer" ints = [int(sp.sympify(s)) for s in sols] kv("Integer roots", ints) kv("Product of roots", sp.prod(ints)) kv("Sum of roots", sum(ints)) # Vieta's try: poly = Poly(p.expr, v) coeffs= poly.all_coeffs() if len(coeffs) == 3: A_, B_, C_ = coeffs kv("Vieta sum (−B/A)", str(-B_/A_)) kv("Vieta prod ( C/A)", str(C_/A_)) finding("Roots satisfy Vieta's formulas") except Exception: pass except Exception as e: fail(f"solve error: {e}") # ── TRIG IDENTITY ───────────────────────────────────────────────────────── elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY): simp = trigsimp(p.expr) r["simplified"] = str(simp) kv("Simplified", simp) kv("Is zero", simp == 0) kv("Is constant", simp.is_number) ops_before = count_ops(p.expr) ops_after = count_ops(simp) kv("Complexity before", ops_before) kv("Complexity after", ops_after) if ops_before > 0: kv("Reduction", f"{100*(ops_before-ops_after)/ops_before:.0f}%") if simp == 0: finding("Expression = 0 for ALL inputs — IDENTITY confirmed") elif simp.is_number: finding(f"Expression is constant = {simp}") r["is_identity"] = (simp == 0) # ── FACTORING ───────────────────────────────────────────────────────────── elif p.ptype == PT.FACTORING: fac = factor(p.expr) flist = factor_list(p.expr) r["factored"] = str(fac) r["factor_list"] = str(flist) kv("Factored form", fac) # Analyse each factor for i, (fi, mult) in enumerate(flist[1]): roots_i = [] try: roots_i = solve(fi, v) except Exception: pass kv(f" factor[{i}]", f"{fi}^{mult} → roots: {roots_i}") r[f"factor_{i}"] = {"expr": str(fi), "mult": mult, "roots": [str(r_) for r_ in roots_i]} # Re-expand to verify reexp = expand(fac) check = simplify(reexp - expand(p.expr)) ok(f"Expand(factor) − original = {check}") r["verified"] = (check == 0) # ── SUMMATION ───────────────────────────────────────────────────────────── elif p.ptype == PT.SUM: k = symbols('k', positive=True, integer=True) n = symbols('n', positive=True, integer=True) res = summation(k, (k, 1, n)) fac = factor(res) r["formula"] = str(res) r["factored"] = str(fac) kv("Formula", res) kv("Factored", fac) # Pattern: f(n) − f(n−1) should equal n diff_check = simplify(res - res.subs(n, n-1)) kv("f(n) − f(n−1)", diff_check) finding(f"Difference property: f(n)−f(n−1) = {diff_check} = n ✓") # Inductive structure kv("f(1)", int(res.subs(n,1))) kv("f(n)/n", simplify(res / n)) finding("Formula is arithmetic mean × n") r["diff_property"] = str(diff_check) # ── PROOF ───────────────────────────────────────────────────────────────── elif p.ptype == PT.PROOF: body = p.meta.get("body", "") if "sqrt(2)" in body.lower(): note("\nFormal proof trace:") steps = [ ("Assume", "√2 = p/q with gcd(p,q)=1"), ("Square", "2 = p²/q² ⟹ p² = 2q²"), ("Deduce", "p² even ⟹ p even ⟹ p = 2m"), ("Substitute", "(2m)² = 2q² ⟹ 4m² = 2q² ⟹ q² = 2m²"), ("Deduce", "q² even ⟹ q even"), ("Contradict", "p,q both even contradicts gcd(p,q)=1"), ("Conclude", "√2 ∉ ℚ □"), ] for step, desc in steps: print(f" {Y}{step:<14}{RST}{desc}") r["proof"] = steps finding("Proof by contradiction: 7-step derivation complete") elif "prime" in body.lower(): note("\nFormal proof trace:") steps = [ ("Assume", "Finitely many primes: {p₁, p₂, …, pₖ}"), ("Construct", "N = p₁ · p₂ · … · pₖ + 1"), ("Observe", "N > pᵢ for all i, so N is not in our list"), ("Factor", "N must have a prime factor q"), ("But", "q cannot be any pᵢ (each leaves remainder 1)"), ("Contradict","No prime divides N — impossible for N>1"), ("Conclude", "Primes are infinite □"), ] for step, desc in steps: print(f" {Y}{step:<14}{RST}{desc}") r["proof"] = steps finding("Euclid's proof: infinite primes by construction") return r def phase_05(p: Problem, prev: dict) -> dict: section(5, "GENERALIZE", "Name the condition, not the cases") r = {} v = p.var # ── LINEAR → general ax + b = 0 ────────────────────────────────────────── if p.ptype == PT.LINEAR: a_, b_ = symbols('a b', nonzero=True) gen = a_*v + b_ sol = solve(gen, v)[0] r["general_form"] = "a·x + b = 0" r["general_solution"] = str(sol) r["governing"] = "a ≠ 0 (if a=0: either 0=b contradiction, or 0=0 trivial)" kv("General form", r["general_form"]) kv("General solution", r["general_solution"]) kv("Governing condition", r["governing"]) finding("x = −b/a iff a ≠ 0") # Show our specific case try: poly = Poly(p.expr, v) A, B = [int(c) for c in poly.all_coeffs()] finding(f"Our case: a={A}, b={B} → x = {-B}/{A} = {Rational(-B,A)}") except Exception: pass # ── QUADRATIC → general formula + discriminant ──────────────────────────── elif p.ptype == PT.QUADRATIC: a_, b_, c_ = symbols('a b c') gen = a_*v**2 + b_*v + c_ gen_sols = solve(gen, v) disc_sym = b_**2 - 4*a_*c_ r["general_form"] = "a·x² + b·x + c = 0" r["quadratic_formula"] = [str(s) for s in gen_sols] r["discriminant_sym"] = str(disc_sym) r["governing_condition"]= "Δ=b²-4ac governs nature of roots" r["cases"] = { "Δ > 0": "two distinct real roots", "Δ = 0": "one repeated real root", "Δ < 0": "two complex conjugate roots", } kv("General form", r["general_form"]) kv("Quadratic formula", r["quadratic_formula"]) kv("Discriminant Δ", disc_sym) for case, meaning in r["cases"].items(): kv(f" {case}", meaning) finding("Nature of roots determined entirely by Δ = b²−4ac") # Our specific discriminant disc_val = prev.get("discriminant", "?") finding(f"Our Δ = {disc_val} → " + ("two real roots" if isinstance(disc_val,int) and disc_val>0 else "double root" if disc_val==0 else "complex roots")) # ── CUBIC → Cardano context ─────────────────────────────────────────────── elif p.ptype == PT.CUBIC: r["general_form"] = "ax³ + bx² + cx + d = 0" r["method"] = "Cardano's formula (via depressed cubic)" r["discriminant"] = "Δ = 18abcd − 4b³d + b²c² − 4ac³ − 27a²d²" r["governing"] = { "Δ > 0": "three distinct real roots", "Δ = 0": "repeated root", "Δ < 0": "one real root, two complex conjugate", } kv("General form", r["general_form"]) kv("Method", r["method"]) for case, meaning in r["governing"].items(): kv(f" {case}", meaning) # General symbolic solution a_,b_,c_,d_ = symbols('a b c d') gen_cubic = a_*v**3 + b_*v**2 + c_*v + d_ try: gen_sols = solve(gen_cubic, v) finding(f"Symbolic solutions exist ({len(gen_sols)} roots)") except Exception: pass # ── TRIG IDENTITY → family ──────────────────────────────────────────────── elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY): r["pythagorean_family"] = { "sin²θ + cos²θ = 1": "Fundamental — all x ∈ ℝ", "1 + tan²θ = sec²θ": "Holds where cos θ ≠ 0", "1 + cot²θ = csc²θ": "Holds where sin θ ≠ 0", } # Verify the family with sympy theta = symbols('theta') checks = { "sin²+cos²": trigsimp(sin(theta)**2 + cos(theta)**2 - 1), "1+tan²": trigsimp(1 + tan(theta)**2 - sec(theta)**2), } for name_, val in checks.items(): kv(f" {name_}", f"= {val} {'✓' if val==0 else '?'}") r["governing"] = "All follow from unit-circle definition: sin²+cos²=1" finding("Pythagorean family — 3 identities, 1 governing principle") # ── FACTORING → difference of squares / sum of cubes family ────────────── elif p.ptype == PT.FACTORING: a_, b_ = symbols('a b') identities = { "a²−b²": factor(a_**2 - b_**2), "a³−b³": factor(a_**3 - b_**3), "a³+b³": factor(a_**3 + b_**3), "a⁴−b⁴": factor(a_**4 - b_**4), } r["factoring_identities"] = {k: str(v) for k, v in identities.items()} kv("Algebraic identities", "") for form, factored in identities.items(): kv(f" {form}", str(factored)) finding("Our problem is an instance of one of these families") r["governing"] = "aⁿ−bⁿ = (a−b)(aⁿ⁻¹+...+bⁿ⁻¹) for integer n≥1" # ── SUMMATION → power sums family ──────────────────────────────────────── elif p.ptype == PT.SUM: k = symbols('k', positive=True, integer=True) n = symbols('n', positive=True, integer=True) power_sums = {} for p_ in range(1, 5): try: s = summation(k**p_, (k, 1, n)) power_sums[f"Σk^{p_}"] = str(factor(s)) except Exception: pass r["power_sums"] = power_sums kv("Power sum family", "") for name_, form in power_sums.items(): kv(f" {name_}", form) r["governing"] = "Faulhaber's formula: Σk^p is degree-(p+1) polynomial in n" finding("Governing condition: Σk^p = poly of degree p+1 in n") finding("Sum of first n integers = n(n+1)/2 is the p=1 case") # ── PROOF → governing theorem ───────────────────────────────────────────── elif p.ptype == PT.PROOF: body = p.meta.get("body", "") if "sqrt(2)" in body.lower(): r["general_theorem"] = "√n ∉ ℚ ⟺ n is not a perfect square" r["governing"] = "Irrationality governed by perfect-square condition" # Verify boundary for n_val in range(1, 10): is_sq = sp.sqrt(n_val).is_integer is_rat = sp.sqrt(n_val).is_rational kv(f" √{n_val}", ("∈ ℚ (perfect square)" if is_sq else "∉ ℚ (irrational)")) finding("√n is rational ⟺ n is a perfect square") return r def phase_06(p: Problem, prev: dict) -> dict: section(6, "PROVE LIMITS", "Find the boundary; state the obstruction") r = {} v = p.var # ── QUADRATIC LIMITS ───────────────────────────────────────────────────── if p.ptype == PT.QUADRATIC: disc_val = prev.get("discriminant", None) r["positive_result"] = ( "For any a,b,c ∈ ℝ with a≠0 and Δ≥0, " "real solutions always exist: x = (−b ± √Δ) / 2a" ) r["negative_result"] = ( "For Δ < 0: no real solutions. " "Two complex conjugate roots exist in ℂ." ) r["degenerate"] = "a=0: not quadratic; becomes linear (one solution)" kv("Positive result", r["positive_result"]) kv("Negative result", r["negative_result"]) kv("Degenerate (a=0)", r["degenerate"]) # Boundary: Δ = 0 a_,b_,c_ = symbols('a b c', real=True) boundary = Eq(b_**2 - 4*a_*c_, 0) kv("Boundary condition", str(boundary)) finding("Boundary Δ=0: double root at x = −b/2a") # Show all roots over ℂ for our problem try: all_sols = solve(p.expr, v, domain=sp.CC) kv("All roots over ℂ", [str(s) for s in all_sols]) r["complex_roots"] = [str(s) for s in all_sols] except Exception: pass # ── LINEAR LIMITS ───────────────────────────────────────────────────────── elif p.ptype == PT.LINEAR: r["positive_result"] = "Unique solution exists whenever a ≠ 0" r["degenerate_a0_b0"] = "0=0: infinitely many solutions (identity)" r["degenerate_a0_bnz"] = "0=b≠0: no solution (contradiction)" kv("Positive", r["positive_result"]) kv("a=0, b=0", r["degenerate_a0_b0"]) kv("a=0, b≠0", r["degenerate_a0_bnz"]) finding("Linear equation has exactly one solution iff leading coefficient ≠ 0") # ── CUBIC LIMITS ───────────────────────────────────────────────────────── elif p.ptype == PT.CUBIC: r["positive_result"] = "Cubic always has at least one real root (degree 3, real coefficients)" r["why"] = "Complex roots come in conjugate pairs; odd degree → ≥1 real root" r["Abel_Ruffini"] = "No general formula in radicals for degree ≥ 5 (Abel-Ruffini theorem)" kv("Always one real root", r["positive_result"]) kv("Why", r["why"]) kv("Degree ≥ 5", r["Abel_Ruffini"]) finding("Cubic: guaranteed ≥1 real root by intermediate value theorem") # ── TRIG IDENTITY LIMITS ───────────────────────────────────────────────── elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY): r["sin_cos_domain"] = "sin²+cos²=1 holds for ALL x ∈ ℝ — no exceptions" r["tan_domain"] = "1+tan²=sec² fails at x = π/2 + nπ (where cos=0)" r["cot_domain"] = "1+cot²=csc² fails at x = nπ (where sin=0)" r["identity_vs_eq"] = "An identity holds universally; an equation holds at specific points" for k_, v_ in r.items(): kv(k_, v_) finding("Pythagorean identity sin²+cos²=1 has NO exceptions in ℝ") # ── FACTORING LIMITS ───────────────────────────────────────────────────── elif p.ptype == PT.FACTORING: e = p.expr r["over_Q"] = "Rational factorization: splits into rational irreducibles" r["over_R"] = "Real factorization: all factors are linear or quadratic" r["over_C"] = "Complex factorization: always splits into linear factors" # Check irreducibility over Q if v: try: poly = Poly(e, v) irred = poly.is_irreducible r["irreducible_over_Q"] = irred kv("Irreducible over ℚ", irred) if irred: finding("Cannot be factored further over ℚ") except Exception: pass try: rr = real_roots(e) ar = all_roots(e) r["real_roots"] = [str(r_) for r_ in rr] r["complex_roots"] = [str(r_) for r_ in ar if not r_.is_real] kv("Real roots", r["real_roots"]) kv("Complex roots", r["complex_roots"]) if r["complex_roots"]: finding("Some roots are complex — irreducible over ℝ too") except Exception: pass # ── SUMMATION LIMITS ───────────────────────────────────────────────────── elif p.ptype == PT.SUM: k = symbols('k', positive=True, integer=True) n = symbols('n', positive=True, integer=True) r["formula_valid"] = "n ≥ 1, n ∈ ℤ" r["n=0"] = "Empty sum = 0; formula gives 0·1/2 = 0 ✓" # Infinite sum diverges try: inf_sum = summation(k, (k, 1, oo)) r["infinite_sum"] = str(inf_sum) kv("Σk to ∞", inf_sum) finding(f"Σk from 1 to ∞ = {inf_sum} — diverges") except Exception: pass # Compare convergence try: harm = summation(1/k, (k, 1, oo)) inv_sq= summation(1/k**2, (k, 1, oo)) kv("Σ 1/k (harmonic)", str(harm)) kv("Σ 1/k² (Basel)", str(inv_sq)) r["convergence_rule"] = "Σ 1/k^p converges iff p > 1" finding("Governing: Σ 1/kᵖ converges ⟺ p > 1 (p-series test)") except Exception: pass # ── PROOF LIMITS ───────────────────────────────────────────────────────── elif p.ptype == PT.PROOF: body = p.meta.get("body", "") if "sqrt(2)" in body.lower(): r["proved"] = "√2 ∉ ℚ" r["generalises"]= "√p ∉ ℚ for any prime p" r["fails_for"] = "√n ∈ ℚ when n is a perfect square" r["governing"] = "√n ∈ ℚ ⟺ n is a perfect square" kv("Proved", r["proved"]) kv("Generalises", r["generalises"]) kv("Fails for", r["fails_for"]) kv("Governing", r["governing"]) finding("Boundary: n a perfect square ↔ √n rational") elif "prime" in body.lower(): r["proved"] = "Infinitely many primes" r["density"] = "π(n) ~ n/ln(n) (Prime Number Theorem)" r["twin_primes"] = "Infinitely many twin primes — OPEN (unproven)" kv("Proved", r["proved"]) kv("Density", r["density"]) kv("Open question",r["twin_primes"]) finding("Euclid's proof: infinite primes; twin-prime conjecture remains open") # ── FINAL ANSWER ───────────────────────────────────────────────────────── print(f"\n{hr('═')}") print(f"{W}FINAL ANSWER{RST}") print(hr('─')) final = _final_answer(p) r["final_answer"] = final print(f" {G}{final}{RST}") print(hr('═')) return r def _final_answer(p: Problem) -> str: v = p.var if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY): try: sols = solve(p.expr, v) return f"Solutions to {p.raw}: {', '.join(str(s) for s in sols)}" except Exception: return "See phase computations" elif p.ptype == PT.FACTORING: try: return f"Factored form: {factor(p.expr)}" except Exception: return "See phase computations" elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY): try: simp = trigsimp(p.expr) return (f"Identity confirmed: simplifies to {simp}" if simp == 0 else f"Simplified: {simp}") except Exception: return "See phase computations" elif p.ptype == PT.SUM: k = symbols('k', positive=True, integer=True) n = symbols('n', positive=True, integer=True) try: s = summation(k, (k, 1, n)) return f"Sum of first n integers = {factor(s)} = n(n+1)/2" except Exception: return "See phase computations" elif p.ptype == PT.PROOF: body = p.meta.get("body", "") if "sqrt(2)" in body.lower(): return "√2 is irrational. Proof by contradiction: assuming p/q (reduced) leads to both p and q even, contradicting gcd(p,q)=1." elif "prime" in body.lower(): return "There are infinitely many primes. Euclid: any finite list p₁…pₖ yields N=p₁…pₖ+1, which has a prime factor outside the list." return "See phase computations above" # ════════════════════════════════════════════════════════════════════════════ # ENTRY POINT # ════════════════════════════════════════════════════════════════════════════ def run(raw: str): prob = classify(raw) print(f"\n{hr('═')}") print(f"{W}DISCOVERY ENGINE{RST}") print(hr()) print(f" {W}Problem:{RST} {Y}{raw}{RST}") print(f" {DIM}Type:{RST} {prob.ptype.value}") print(f" {DIM}Variable:{RST} {prob.var}") print(hr('═')) if prob.ptype == PT.UNKNOWN: print(f"{R}Could not parse. Try: 'x^2 - 5x + 6 = 0' or 'factor x^4-16'{RST}") return g1 = phase_01(prob) g2 = phase_02(prob, g1) g3 = phase_03(prob, g2) g4 = phase_04(prob, g3) g5 = phase_05(prob, g4) g6 = phase_06(prob, g5) # Summary print(f"\n{hr()}") print(f"{W}PHASE SUMMARY{RST}") print(hr('·')) titles = {1:"Ground Truth", 2:"Direct Attack", 3:"Structure Hunt", 4:"Pattern Lock", 5:"Generalize", 6:"Prove Limits"} for i, (g, title) in enumerate(zip([g1,g2,g3,g4,g5,g6], titles.values()), 1): fa = g.get("final_answer","") line = fa[:60] if fa else ( str(g.get("solutions", g.get("factored", g.get("formula", g.get("simplified", "✓")))))[:60] ) print(f" {PHASE_CLR[i]}{i:02d} {title:<16}{RST} {line}") print(hr('═')) TESTS = [ ("x^2 - 5x + 6 = 0", "Quadratic with integer roots"), ("2x + 3 = 7", "Linear equation"), ("x^3 - 6x^2 + 11x - 6 = 0", "Cubic with 3 integer roots"), ("sin(x)^2 + cos(x)^2", "Pythagorean identity"), ("factor x^4 - 16", "Difference of squares chain"), ("sum of first n integers", "Classic summation"), ("prove sqrt(2) is irrational", "Irrationality proof"), ] def run_tests(): print(f"\n{hr('═')}") print(f"{W}DISCOVERY ENGINE — TEST SUITE{RST}") print(f"{DIM}Running {len(TESTS)} problems{RST}") print(hr('═')) passed = 0 for raw, desc in TESTS: print(f"\n{B}{'─'*60}{RST}") print(f"{B}TEST: {desc}{RST}") print(f"{DIM}{raw}{RST}") try: run(raw) ok(f"PASSED: {desc}") passed += 1 except Exception as e: fail(f"FAILED: {desc} — {e}") traceback.print_exc() print(f"\n{hr('═')}") print(f"{G if passed==len(TESTS) else Y}Results: {passed}/{len(TESTS)} passed{RST}") print(hr('═')) if __name__ == "__main__": args = sys.argv[1:] if not args: print(__doc__) print(f"\n{W}Available test problems:{RST}") for raw, desc in TESTS: print(f" {DIM}{raw:<40}{RST} {desc}") elif args[0] == "--test": run_tests() else: run(" ".join(args))