Tutorial: Maximum Results, Minimum Code

Setup

Two lines. That is all it takes to be ready.

pip install -e .

from jugeo.easy import prove, bugs, equiv, ideate, carry

That single import gives you five capabilities: bug detection, formal verification, equivalence checking, mathematical ideation, and proof-carrying code generation. The rest of this tutorial shows you each one.

Find Bugs Instantly

Everyone has bugs. bugs() finds them in seconds. Pass it a string of Python source and get back a structured list of problems — each one with a line number, a category, a plain-English message, and a suggested fix.

from jugeo.easy import bugs

result = bugs('''
def process(data=[]):
    try:
        return data
    except:
        pass
''')

print(f"Found {result.count} bugs")
for bug in result.items:
    print(f"Line {bug.line}: {bug.message}")

Verify Real Code

prove() takes Python source and verifies it against its own spec_* functions — any function whose name starts with spec_ is treated as a property to be proved. You get a rich structured result telling you exactly which properties were verified, at what trust level, and how long it took.

Here is a complete merge sort implementation. Every spec_* function is a separate property. All twelve propositions are verified in one call.

from jugeo.easy import prove

result = prove('''
def inc(x):
    return x + 1

def spec_inc(result, x):
    return result > x
''')

print(result)
print(f"Verdict: {result.verdict}")
print(f"Trust:   {result.trust}")
print(f"Props:   {result.propositions[0]}/{result.propositions[1]}")
print(f"Site:    {result.coordinates} coordinates, H1={result.H1}")

Check Equivalence

Have two implementations of the same thing? equiv() tells you whether they are semantically identical — or produces a concrete counterexample when they are not.

Equivalent case

def deduplicate(items):
    """Remove duplicates,
    preserving order."""
    seen = set()
    result = []
    for item in items:
        if item not in seen:
            seen.add(item)
            result.append(item)
    return result

def deduplicate(items):
    """Remove duplicates,
    preserving order."""
    return list(dict.fromkeys(items))

from jugeo.easy import equiv

result = equiv(
    '''
def deduplicate(items):
    """Remove duplicates preserving order — using a set."""
    seen = set()
    result = []
    for item in items:
        if item not in seen:
            seen.add(item)
            result.append(item)
    return result
    ''',
    '''
def deduplicate(items):
    """Remove duplicates preserving order — using dict.fromkeys."""
    return list(dict.fromkeys(items))
    '''
)

print(result)  # EquivResult(EQUIVALENT)

Non-equivalent case

Now try two deduplication strategies where one sorts first and one does not. They produce identical elements but in a different order — that is enough to make them non-equivalent, and JuGeo will tell you exactly why.

from jugeo.easy import equiv

result = equiv(
    "def f(x): return x + 1",
    "def f(x): return x + 2",
)
print(result)
print(f"Counterexample: {result.counterexample}")

Verify a Neural Network

JuGeo can verify shape-safety, numerical stability, and mathematical invariants of tensor code. Here is a complete scaled dot-product attention implementation. One call to prove() verifies six properties simultaneously.

from jugeo.easy import prove

LINEAR_LAYER = '''
def relu(x):
    return x if x > 0 else 0

def layer(x, weight, bias):
    return relu(x * weight + bias)

def spec_relu_non_negative(result, x, weight, bias):
    return result >= 0
'''

result = prove(LINEAR_LAYER)
print(result)
print(f"Verdict: {result.verdict}")
print(f"Trust:   {result.trust}")
print(f"Props:   {result.propositions[0]}/{result.propositions[1]}")

Ideate New Mathematics

ideate() takes a research topic and generates novel theorems: conjectures, existence results, impossibility arguments, and characterization theorems. Each comes with a novelty score, a confidence estimate, and an optional proof sketch.

This is not a search engine. It synthesizes new mathematical content by navigating the semantic space of known results and extrapolating along productive directions.

from jugeo.easy import ideate

result = ideate("Topological methods for analyzing neural network loss landscapes")

print(f"Generated {len(result.theorems)} theorems:\n")
for thm in result.theorems:
    print(f"  [{thm.kind}] {thm.statement}")
    print(f"  Novelty: {thm.novelty_score:.2f},  Confidence: {thm.confidence:.2f}")
    if thm.proof_sketch:
        print(f"  Sketch: {thm.proof_sketch[:200]}...")
    print()

Proof-Carrying Code

carry() verifies your code and then bundles the source with a certificate. Anyone downstream can re-verify the certificate in O(1) time — a hash check, not a re-proof. Ship source and cert together; the certificate travels with the code.

from jugeo.easy import carry

MY_CODE = '''
def inc(x):
    return x + 1

def spec_inc(result, x):
    return result > x
'''

source, cert = carry(MY_CODE)
print(source.splitlines()[0])
print(cert["verdict"])
print(cert["trust"])
print(cert["certificate_hash"][:16])

Going Deeper

The five functions above cover the vast majority of what most users need. But if you want the full power of JuGeo's internal machinery — custom sites, explicit judgment algebra, descent strategies, cohomology classes — it is all there.

# The full public low-level API — use this when jugeo.easy is not enough
from jugeo.geometry.site import Coordinate, CoordinateKind, SiteBuilder, Morphism, MorphismKind
from jugeo.geometry.covers import CoverBuilder
from jugeo.geometry.descent import DescentEngine, DescentStrategy
from jugeo.evidence.trust import TrustAlgebra, TrustLevel
from jugeo.solver.router import SolverRouter, RoutingStrategyKind

With the internal API you can build semantic sites by hand, create judgments with custom evidence bundles, compose trust algebraically, run the descent engine directly, and inspect the cohomology classes that encode why a proof failed. Everything in jugeo.easy is built on top of these primitives.

What You Just Learned

Five functions. One import. Everything returns a structured result with no magic strings.