Scryer | woflo

Models are good at guessing what might be true. Scryer gives those guesses somewhere exact to land. It's a symbolic engine for research: it works over exact mathematical objects, derives what it can, and says where it gets stuck. Some results come with evidence you can replay.

why

A model can notice a pattern or choose a useful next question. Its confidence shouldn't do the algebra.

01 / guess agent chooses what to try

02 / work Scryer exact objects & operations

03 / result established or still open, with a reason

Both outcomes can inform the next guess, but only established results become facts.

what exists now

It works with rationals and algebraic numbers, fields, polynomials, matrices, logic, graphs, optimisation, dynamics, and other domains.

Ask what follows from an object, or work backwards from laws to objects that satisfy them.

A generic construction space can reach the same mathematical object by different routes. That collision gives an identity to inspect.

Scryer can also search for candidate relations and counterexamples, and keep track of open conjectures.

a few outputs

These screenshots come from an artifacting tool built on Scryer. The document supplied the equations; Scryer derived the details.

Scryer reading f sub n = 440 times 2 to the n over 12: a plotted curve and a table with exact values 440, 880, and 1760 at n = 0, 12, and 24 — frequency curve · 440, 880 and 1760 Hz at n = 0, 12 and 24.

Scryer reading a piecewise function: t squared for t at most one and two minus t above one, with both curves meeting at one — piecewise rule · the branches meet at t = 1.

Scryer returns the exact roots three plus or minus two i for x squared minus six x plus thirteen equals zero; the artifacting tool plots the conjugate pair — complex roots · 3 ± 2i.

the important rule

Scryer can say no.

If it runs out of search budget, lacks the right representation, or needs mathematics it doesn't have, the result should say so. An unproved claim stays unproved.

An exact calculation can still start from faulty assumptions or answer the wrong question. Those limits should stay visible.

where it's headed

Verification came first. The work now is to let an agent build exact objects, search through them, and use what it finds to choose its next question.

A small proof and search system is testing that idea. Suggestions can steer the search. Only checked results are treated as facts; an open goal still shows what needs proving.

a tiny example of the idea

The search recovered the familiar identity √(3 + 2√2) = 1 + √2 when two constructions reached the same exact number.

use it

Public research access lets agents use Scryer through MCP tools.

Public research access details and bearer tokens →

underneath

The engine works with distinct mathematical structures that share arithmetic machinery. Each domain adds its own rules. Where implemented, certificates and proof DAGs make results replayable.

When one of those results looks odd, there's a trail to follow.