Arend 1.12.0 released

This release includes a major internal overhaul of the universe/level system, an opt-in binary caching mode for the CLI, and substantial additions to arend-lib, most notably in algebraic geometry and analysis.

Language updates:

• Introduce types not bounded by universe levels.
• Introduce classes not bounded by universe levels, with a local override available when a definition needs to be pinned to a finite level.
• Prefix application of infix operators is now forbidden. Applying an infix operator to a single argument is instead interpreted as a right section.

Plugin updates:

• Updated IntelliJ platform support to 2025.3, then to 2026.2.
• Added basic Arend support for the JetBrains Educational plugin (course builder, project generator, and task checker).
• Fixed a UI freeze in the custom searcher, formatter performance issues, and the Arend Messages panel.

CLI updates:

• Added an opt-in binary cache (.arc) serialization mode for faster incremental rechecking: pass --serialize to persist typechecked results, and -r/--recompile to ignore existing caches.
• Added console query tooling: -ss (symbol search), -ps (proof search), -fu (find usages), -ch (class hierarchy), and -sc (scope), all with --json output support.
• The proof searcher, previously IDE-only, is now available in the console app.
• REPL improvements: Ctrl+J (multi-line input), Ctrl+C (clear line), Ctrl+D (quit), -L support, and module preloading.
• Added progress indication to the console app and support for typechecking individual definitions from the CLI.

arend-lib:

• Introduce scheme sites, affine opens, affine schemes, and general schemes built from a scheme site.
• Construct Spec and Proj; prove Spec is a reflective embedding of CRing^op into scheme sites and check the sheaf condition for the structure sheaf on Spec R.
• Define locally ringed locales and construct a fully faithful functor and equivalence of morphisms between scheme sites and locally ringed locales; prove every scheme can be reconstructed from a scheme site.
• Refactor locales and sites, including dense sites and preorder sites; prove the category of ringed locales is univalent.
• Cauchy product of power series; make exp and log(1+x) into functions with full analytic properties; define sin and cos and prove cos π = -1.
• Make complex numbers a Banach algebra.
• Define Noetherian rings and prove products of Noetherian rings are Noetherian; define Bar-Noetherian rings, bar induction, and prove the fan theorem.
• Prove Hilbert’s basis theorem for Bar-Noetherian rings.
• Define tensor products of modules and of algebras.
• Refactor Heyting algebras, complete lattices, and the localization of rings and monoids.
• Replace Equiv with QEquiv and IsEquiv throughout the library.
• Refactor the hierarchy of substructures and group representation theory.
• Add natarith/intarith tactics extending the linarith-style solver, including Nat div/mod support.

• 2026 1
• 2025 1
• 2024 1
• 2022 3
• 2021 2
• 2020 5
• 2019 3