Initialize environment
Run the Windows installer and startup scripts from the maintained repo, or use Docker Compose directly.
.\INSTALL_QUANTHOR.bat
.\START_QUANTHOR.bat
Tier 4 - mathematical verification - public pre-alpha
Mathematical verification, routed with supervision.
QuaNThoR helps students and mathematicians move between theorem intent, conservative Mizar drafts, formal verifier feedback, local proofreading, optional retrieval context, and operational audit traces.
Mizar verification remains the formal check. Human mathematical review remains required. AI is traceability support, not proof authority.
Theorem-aware
Container-first
Route-intelligent
SEL-2.0
Start in 15 minutes
Container-first local execution, no classroom token handling.
Official classroom use must not require students or teachers to provide raw API keys, local model secrets, or unmanaged provider routes.
Submit Mizar or intent
Use a full Mizar article for verification, or plain language for conservative draft routing.
environ ...
begin ... end;
Route and correct
The router chooses proofread, draft_mizar, verify_mizar, or needs_clarification, then executes only when asked.
proofread -> draft_mizar
verify_mizar -> review
Review evidence
Read success, failure, parsed errors, raw verifier output, and optional audit traces before accepting any result.
status: success | failure | error
Real interface model
Three panels, runtime strip, explicit review boundary.
The landing must represent the actual Flask workbench, not a generic AI dashboard.
Mizar: runtime checked
Proofreader: school-heuristic
HippoRAG: optional
Timeout: 60s default
Route automatically
Paste prose, theorem intent, or Mizar. Optionally include HippoRAG context and neutrosophic audit.
text | query | prompt | code
Verify a proof
Submit a complete Mizar article to the verifier and inspect structured errors plus raw output.
POST /verify
Draft from a request
Create a conservative Mizar draft with clarification questions and editing suggestions.
POST /draft
API logical functions
Represent the real endpoints and nothing beyond them.
Formal verifier path
Accepts a complete Mizar article and returns success, failure, error, parsed errors, and raw verifier output.
Intent router
Classifies requests into proofread, draft_mizar, verify_mizar, or needs_clarification with optional execution.
Local proofreader
Uses a conservative school-heuristic proofreader for grammar, punctuation, and clarity support.
Optional context
HippoRAG can provide retrieval context when enabled; retrieval context does not verify formal correctness.
Operational audit
Reports trace layers and recommendation signals. It does not certify a theorem.
Relation audit
Classical zero-dependency audit over retrieval relations; not quantum computation and not a formal proof.
Evidence boundary
I -> I_system^S -> D_f -> dF -> i_fractal
QuaNThoR keeps operational uncertainty, structural drift, dynamic falsification, and fractal residue separate. The audit trace supports review; it does not replace Mizar or a qualified human reader.
- Pre-alpha / in development.
- Education, research, simulation, classroom training, and supervised learning only.
- No production, clinical, regulatory, enforcement, safety-critical, or autonomous proof authority claim.
- No Ollama Cloud, uncensored local AI, raw-token student flow, or unknown classroom agent provider as official school route.