Skip to content

Mathematics input via the operating system

Instead of relying on an editor to enable Unicode math input, your operating system can provide this feature across all applications. This can be accomplished through the operating system's keyboard input methods or a text expander.

If your favorite non-editor Unicode math input method is not listed on this page, feel free to email Castedo or send a pull request.

Cross-platform

Espanso.org text expander

You can use the Espanso package for Lean or configure your own, similar to this custom config.

macOS

See Math input method in Mac OS X.

Linux

These notes document two approaches to math input on Linux:

  1. XCompose: the older, classic configuration standard from the X keyboard extension (XKB).

  2. Intelligent Input Bus (IBus): a newer technology that has become the default input method for GNOME Desktop, Fedora, RHEL, and Ubuntu.

Which should you choose? Here is some Lean code for a quick evaluation:

#eval if think you (should XCompose)
  then XCompose
  else IBus

If you want more food for thought, here are some questions to consider:

  • Will IBus be difficult to set up? Look at the instructions for IBus. If it seems like it will be difficult to set up on your system, then it's probably not worth it, and you should just go with XCompose.

  • Are you new to Lean and still learning which abbreviations correspond to which math symbols? The Lean input method in the package ibus-table-other will display completions and symbols in a pop-up window as you type.

  • Do you type in multiple languages? Do you sometimes input math in English and, at completely different times, input non-math in non-English with non-English letters/symbols? If so, you might prefer input mode switching with IBus.

Lean Zulip Topic References