Formal-System Assistant Toolkit

Verify. Analyse.
Process.

Hypatia is an open-source ecosystem for verifying, analysing, and processing user-defined formal systems crafted in the Hypatia language and its evolving dialects.

Hofstadter's MIU System

$Hypatia Sifr $:
$Lingua MIU $:

  $Alphabetum M I U x y $.

  $Lexicon M I U $.
  $Mutabilia x y $.

  $Principium MI $: MI $.
  $Regula I   $: xI    $- xIU $.
  $Regula M   $: Mx    $- Mxx $.
  $Regula III $: xIIIy $- xUy $.
  $Regula UU  $: xUUy  $- xy  $.

  $Productum MIU $:
    MIU
  $ex
    $Probatione
      $Assumo    MI        $per $Principium MI $.
      $Assumo    MI $- MIU $per $Regulam I $cum x $= M $.
      $Consequor       MIU $.
    $.
  $.

$. $.

$Hypatia Sifr $:
$Lingua SKI $:

  $Alphabetum S K I x y z $.
  $Intervalla \sp \th $.

  $Lexicon S K I $.
  $Mutabilia x y z $.

  $Regula I $: I x     $- x       $.
  $Regula K $: K x y   $- x       $.
  $Regula S $: S x y z $- x z y z $.

  $Derivatio SKK2I $:
    S K y z $- z
  $ex
    $Probatione
      $Praemitto S K y z $.
      $Consequor K z y z $ex $Regula S $cum x $= K $.
      $Consequor   z     $ex $Regula K $cum x $= z
                                        $,   y $= y z $.
    $.
  $.

$. $.

$Hypatia Sifr $:
$Lingua A::B $:

  $Alphabetum A B # x y $.
  $Intervalla \sp \th $.

  $Lexicon A# #A B# #B $.
  $Mutabilia x y $.

  $Regula A##A $: x A# #A y $- x       y $.
  $Regula B##B $: x B# #B y $- x       y $.
  $Regula A##B $: x A# #B y $- x #B A# y $.

  $Derivatio Simp $:
    B# A# #B #A $- $Vacuum
  $ex
    $Probatione
      $Praemitto B# A# #B #A $.
      $Consequor B# #B A# #A $ex $Regula A##B
                             $cum x $= B# $, y $= #A $.
      $Consequor       A# #A $ex $Regula B##B
                             $cum x $= $Vacuum
                             $,   y $= A# #A $.
      $Consequor $Vacuum     $ex $Regula A##A
                             $cum x y $= $Vacuum $.
    $.
  $.

$. $.

About

A language and toolkit for explicit formal reasoning

The Language

The Hypatia language is a foundation-agnostic host language for defining and studying formal systems. It is organised as a stratified tower of dialects, from the minimal core Sunya upward through increasingly ergonomic constructs, whose meaning is defined by translation to lower layers. At the level of the formal systems it encodes, Hypatia, like Metamath, treats statements as sequences of symbols without imposing a fixed object-level syntax or built-in semantic interpretation. Like Mizar, it favours an intelligible self-explanatory syntax readable by humans and tools alike.

The Name

Hypatia is named after Hypatia of Alexandria (c.350/370–415 AD), mathematician, astronomer, and head of the Neoplatonic school. The components of the suite bear equally classical names: the validator Aristarchus, after Aristarchus of Samothrace (c. 220–143 BC), grammarian and head librarian of the Library of Alexandria; the analyser Anaxagoras, after Anaxagoras of Clazomenae (c. 500–428 BC), philosopher of mind and matter; the processor Metis, after the Titaness of wisdom in Greek mythology; and the language server Pythia, after the high priestess of the temple of Apollo at Delphi.

The Toolkit

All Hypatia implementations realise the same command-line suite for checking, analysing, transforming, and certifying formal artefacts. The architecture centres on a small verifier kernel and keeps richer processing facilities outside the core verification boundary.

The Ecosystem

The Hypatia ecosystem separates the normative language from its implementations, documentation, libraries, and companion tools. The workspace joins these repositories through curated snapshots recording the state and exact commit of each included component.

Features

What Hypatia is designed to support

Mechanised Verification

Check that every proof step follows from the inference rules declared by the formal-system fragment and is valid under the active Hypatia dialect, keeping the acceptance path explicit.

Dialect Tower

Work at different levels of abstraction with explicit semantics-preserving translations from richer dialects to the Sunya core. Each layer reduces to a simpler verification target.

Theory Neutrality

Encode formal systems without imposing a background logic, set theory, type theory, or ambient axioms on the host language. Foundational assumptions remain explicit in the encoded system.

Proof Certification(planned)

Generate explicit correctness certificates witnessing successful verification, supporting trusted verification pipelines and independent audit trails.

Transformations(planned)

Normalise and translate documents to and from Metamath, Mizar, Isabelle, Lean, and other frameworks, enabling interoperability across formal ecosystems.

Language Server(planned)

Provide IDE integration through the Language Server Protocol, supporting real-time diagnostics, navigation, and other language-aware editor services.

Dialects

A tower of formal languages

The dialect tower is a stratified hierarchy in which each higher layer is required to admit a semantics-preserving translation towards the layers below it, so that richer notation can be reduced to progressively simpler verification targets. Sunya forms the minimal core at the base of the tower, and its semantics is defined within Sunya itself.

Sunya, Sifr, and Zero, the three base dialects currently defined by the language, take their names from historical words for ‘zero’ in Sanskrit, Arabic, and Latin, respectively, echoing the progression from the minimal core towards increasingly ergonomic notation.

Zero

experimental

Ergonomic dialect with richer sequencing and higher-level proof structuring constructs. Under active design; not yet stable.

Sifr

syntactic sugar

Purely syntactic layer over Sunya with no additional expressive power. Every Sifr construct desugars to Sunya deterministically.

Sunya

stable core

The stable minimal foundation of the tower. Explicit and verbose by design; easy to verify by both automated tools and direct human inspection.

Coming Soon