Plainv0 experimentProject map

English-friendly · Lean-backed

A sentence.
One meaning.

Write a small, fixed form of English. See its structure. Make the meaning precise enough for Lean.
Plain is a working name.

Try a sentence

Browser model
Ctrl / ⌘ + Enter
Examples

Meaning

Ready
This JavaScript model previews parsing and closed arithmetic. It does not run Lean or its kernel. It resolves earlier Plain definitions only, not constants from a Lean environment. The Lean sketch shows the intended translation. Browser limits: 8,000 input characters, 100 sentences, 64 nesting levels, and 10,000 calculated digits.






01 / Interface
Clarity is the syntax
A fixed vocabulary, explicit nesting, and useful errors. No guessing what the writer meant.
Small grammar
Definitiondefine name as expression.
Checkcheck proposition.
Expressionnumber · name · the sum of A and B
the product of A and B
ComparisonA is equal to B
A is greater than B
A is less than B
Logicboth (P) and (Q)
either (P) or (Q)
not (P)
One sentence, one tree
  • Use names instead of “it,” “this,” or “that”
  • Use parentheses for nested structure
  • State the exact comparison
  • No inferred units or guessed synonyms
  • Close each sentence with a period
Overlap
Interface Library
Every phrase is a typed signature, not just a writing rule. Names are case-sensitive and follow [a-z][a-z0-9_]*.
Too open-ended
Check it is about twenty.
A precise form
check total is equal to 20.







Project map
Four views. Shared edges.
The views describe the same project. They overlap wherever a language feature becomes a usable, checked building block.
Interface
Grammar · diagnostics · canonical text
Implementation
Tokenizer · tree · typed Lean · kernel
Application
Arithmetic specifications · exact requirements
Library
Nat · comparisons · logic · later dictionaries
Phrase signatures Interface + LibraryClosed checks Application + Implementation