Nexeron.Mathman 0.6.0

A proof-obligation-driven, exact neuro-symbolic mathematical researcher powered by NexeronLRS.

English · 简体中文 · Русский · Français · Deutsch · 日本語 · Español

Mathman 0.6.0 replaces benchmark-shaped method invention with a structural research agenda. It classifies open obligations—normalization, elimination, invariant discovery, decomposition, degree lowering, independent verification, counterexample audit—then expands only the highest-value frontier that is not dominated by a cheaper or stronger state.

The 0.6.0 research system also prevents a finite-domain witness from masquerading as an invented method. When a target still depends on search variables, Mathman first runs an observable r1 algebraic research wave. Enumeration is permitted only after bounded algebraic elimination fails. It does not claim universal mathematical intelligence or completeness.

Parameter-free Mathman Script 3

@mathman 3
@problem symmetric_polynomial
@title Symmetric polynomial

@var x integer 1..50
@var y integer 1..50
@where x + y = 23
@where x * y = 132
@where x < y

@target square_sum = x^2 + y^2
@show x, y, answer, method
@end

There are no search parameters in this script. Before compilation, the automatic controller measures domain size, variable and constraint structure, expression complexity, continuous-domain cost, raw logic, and cognitive tasks. It selects the smallest bounded starting budget appropriate for the measured difficulty. Explicit @option values remain supported as deliberate overrides. All 17 bundled examples use this Script 3 model without manual search-budget parameters.

What changed in 0.6.0

General research agendas, not exercise templates

• MathResearchAgendaPlanner derives obligations from expression complexity, polynomial degree, equality structure, variable roles, and current method coverage. It never sees a problem id or benchmark filename.
• The invention beam uses Pareto-style dominance pruning across score, expression complexity, and derivation length, stopping same-family syntax variants from consuming research breadth.
• Exact multivariate polynomial normal form is a reusable strategy alongside constraint solving, invariant discovery, factorization, calculus, topology, tensor, and group kernels.
• Bounded enumeration is a named lowest-priority obligation, not the mechanism labeled as research.

Exact polynomial-map research and the Jacobian counterexample

ExactPolynomialEngine implements normalized rational-coefficient polynomials over declared variables, exact identity checks, degree, differentiation, bounded exact Jacobian determinants, composition, two-sided inverse verification, and collision certificates. These operations do not sample points or use floating-point tolerances.

The bundled jacobian-counterexample-certificate.mathman replays the 2026 three-dimensional counterexample: it independently proves det JF = -2 and verifies distinct rational preimages with one image. The resulting CertifiedCounterexample status is a two-part exact disproof certificate, not a finite search claim. The published map and its exact-arithmetic audit are documented in Gao's self-contained account.

Cohesive runtime modules

MathmanEngine.cs is reduced from 1,271 to about 520 lines. Research coordination, runtime policy, and cognitive auxiliary operations now live in three cohesive files in the existing Runtime directory—no class-per-folder hierarchy and no fragmentation of the main solve loop.

What changed in 0.5.1

Algebra before enumeration

• A structural research assessment measures residual target variables, equality constraints, and finite-domain search cost before the reasoner visits domain facts.
• Script 3 automatically triggers r1/r2 research while exact equality elimination can still make progress.
• The research engine now applies the general identity p₂ = e₁² - 2e₂ to complete square sums, rather than solving individual variables and discovering an invariant by trial.
• Variable-free candidates receive a strong ranking bonus; syntactic route count can no longer make several witness-enumerating methods look like independent mathematical innovation.

Machine-checked algebraic certificates

Every claimed algebraic shortcut is replayed from the declared target. Each step must match a trusted structural identity, solved equality, or exact constraint substitution, and the chain must end at the method expression with no declared variables remaining. A certified chain compiles to a separate algebraic proof predicate whose arithmetic remains visible as BuiltinEvaluation nodes.

When that predicate succeeds, bounded counterexample enumeration is explicitly reported as DeferredToEnumerationFallback. The final answer contains the invariant value and research method, not dozens of incidental (x,y,z) witnesses.

What changed in 0.5.0

Intelligent automatic dynamic control

Script 3 runs a two-stage controller:

1. Preflight profiling classifies the problem as Basic, Standard, Advanced, or Research and derives inference, deliberation, audit, continuous-solver, and invention budgets.
2. Evidence feedback decides whether the useful next action is to retry deduction with a larger budget, invent a structurally distinct method, or accept the audited result.

A conclusive proof is no longer replayed merely because route diversity is low. Low diversity asks the invention engine for a different method; only an inconclusive or conflicting search justifies a larger deduction budget.

The complete plan, preserved overrides, runtime decisions, proof-pass count, constructed arguments, cache hits, quarantine count, and research-round count are exposed in the cognitive report.

Shared target witnesses

Version 0.4 compiled every candidate method with a private copy of:

• domain enumeration;
• all problem constraints;
• original target evaluation;
• candidate evaluation and equivalence checks.

Version 0.5 compiles the domain, constraints, and original target once into a target-witness rule. Every method and counterexample rule reuses that witness and contributes only its own independent calculation and proof obligation. This removes repeated work without hiding evidence.

Successful deterministic calculations still appear as first-class BuiltinEvaluation nodes in the observable proof graph.

Tabled proof and deterministic evaluation reuse

The goal-directed reasoner now tables completed non-ground subgoals as grounded arguments and re-projects them into later standardized rule invocations. Pure built-in evaluations are cached by normalized input shape and re-unified with current variables. This allows methods to share facts, constraint witnesses, and exact arithmetic while preserving their distinct top-level proof routes.

Denser invention

The invention engine now:

• parses equality constraints once per research wave;
• continues from previously admitted frontier methods instead of restarting at the target root;
• ranks by constraint utility, novelty, simplicity, remembered strategy quality, and evidence cost;
• selects representatives from distinct strategy families before admitting same-family variants;
• retains deterministic fingerprints, complete derivation steps, bounded counterexample audits, and transferable strategy-family memory.

Adaptive NexeronLRS use

Mathman still uses the complete NexeronLRS stack—cortical recruitment, adaptive rule memory, metacognition, scenarios, counterfactuals, abduction, truth maintenance, demonstration learning, self-modifying programs, petals, and proof production—but expensive diagnostic mechanisms are activated by task requirements and evidence rather than forced into every ordinary calculation.

Assurance model

Mathman has two explicit assurance paths.

For an exact algebraic research method, Mathman requires:

1. a continuous derivation starting at the declared target;
2. every transformation to be licensed by the trusted rewrite system and declared equalities;
3. a final expression independent of all declared search variables;
4. observable deterministic evaluation of that expression.

Only methods satisfying all four requirements may bypass enumeration. Other generated or hinted methods retain the bounded 0.5 obligations:

1. a shared witness satisfying the declared domain and every constraint;
2. exact or bounded-numerical evaluation of the declared target;
3. an independently compiled candidate evaluation;
4. target/candidate equivalence;
5. a batched counterexample search.

A supported counterexample removes the candidate solution rule from the live knowledge base. A NoCounterexampleFound result remains explicitly bounded by declared domains, numerical witnesses, and inference budgets; it is not mislabeled as a universal theorem certificate.

Compatibility

• Mathman Script 1 remains supported as the legacy explicit-route language.
• Mathman Script 2 remains source compatible with the 0.4 orchestration model.
• Mathman Script 3 is the recommended language and enables automatic control by default.
• @option auto-control = false disables Script 3 profiling.
• Any explicit option overrides only the corresponding generated value.

See Mathman Script 3 Development Guide, 0.6 architecture, 0.6.0 upgrade report, and 0.5.1 upgrade report.

Mathematical kernels

Mathman includes deterministic kernels for:

• arithmetic, comparisons, number theory, elementary functions, combinatorics, GCD and LCM;
• symbolic simplification, differentiation, rule-based integration, and limits;
• exact rational multivariate polynomial normalization, identities, maps, Jacobians, inverse and collision certificates;
• numerical differentiation, integration, root search, and RK4 ODE solving;
• bounded continuous systems with correlated numerical witnesses;
• finite topology;
• numerical tensors and matrices;
• finite groups.

New kernels are registered through BuiltinExtensionRegistry and remain observable proof steps.

Run

Requirements: .NET 9 SDK and a UTF-8 terminal.

git clone https://github.com/LytharaLab/NexeronMathman.git
cd NexeronMathman
dotnet build Nexeron.sln --configuration Release
dotnet run --project Nexeron.Mathman -- --self-test
dotnet run --project Nexeron.Mathman -- solve Nexeron.Mathman/Examples/symmetric-polynomial.mathman
dotnet run --project Nexeron.Mathman -- solve Nexeron.Mathman/Examples/jacobian-counterexample-certificate.mathman

Interactive commands:

:demo
:self-test
:load Nexeron.Mathman/Examples/integer-pair.mathman
:answer
:details
:compiled
:trace
:passes
:stats
:save result.generated.nex

Scope

Mathman is experimental. Search, invention, continuous witnesses, and audits are bounded and observable. It is not yet a complete computer algebra system, proof assistant, equality-saturation engine, Gröbner-basis system, or universally quantified theorem prover. The v0.6.0 control system improves how implemented capabilities are allocated; it does not pretend that missing mathematics can be recovered by increasing a numeric budget.