Litex: The First Formal Language Learnable in 1-2 Hours

Summary

Litex: Simply Scale Formal Reasoning In AI Era version v0.1.10-beta (not yet ready for production use) Jiachen Shen and The Litex Team Litex: The First Formal Language Learnable in 1–2 Hours Simplicity is the ultimate sophistication. – Leonardo da Vinci Litex(website) is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo!). It ensures every step of your reasoning is correct, and is actually the first reasoning formal language (or formal language for short) that can be learned by anyone in 1–2 hours, even without math or programming background. Making Litex intuitive to both humans and AI is Litex's core mission. This is how Litex scales formal reasoning: by making it accessible to more people, applicable to more complex problems, and usable by large-scale AI systems. These benefits stem from Litex's potential to lower the entrance barrier by 10x and reduce the cost of constructing formalized proofs by 10x, making formal reasoning as natural as writing. Here is a comparison between Litex and traditional formal language Lean. Litex Lean 4 let x R, y R: 2 * x + 3 * y = 10 4 * x + 5 * y = 14 2 * (2 * x + 3 * y) = 2 * 10 = 4 * x + 6 * y y = (4 * x + 6 * y) - (4 * x + 5 * y) = 2 * 10 - 14 = 6 2 * x + 3 * 6 = 10 2 * x + 18 - 18 = 10 - 18 = -8 x = (2 * x) / 2 = -8 / 2 = -4 import Mathlib.Tactic example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁] have h₄ : 4 * x + 6 * y = 20 := by linear_combination 2 * h₁ have h₅ : (4 * x + 6 * y) - (4 * x + 5 * y) = 20 - 14 := by rw [h₄, h₂] have h₆ : (4 * x + 6 * y) - (4 * x + 5 * y) = y := by ring have h₇ : 20 - 14 = 6 := by norm_num have h₈ : y = 6 := by rw [←h₆, h₅, h₇] have h₉ : 2 * x + 3 * 6 = 10 := by rw [h₈, h₁] have h₁₀ : 2 * x + 18 = 10 := by rw [mul_add] at h₉ simp at h₉ exact h₉ have h₁₁ : 2 * x = -8 := by linear_combination h₁₀ - 18 have h₁₂ : x = -4 := by linear_combination h₁₁ / 2 exact ⟨h₁₂, h₈...