4 ms·

Litex is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo! https://github.com/litexlang/golitex https://github.com/litex

Litex is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo! https://github.com/litexlang/golitex https://github.com/litexlang/golitex). 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 human and AI is the mission of Litex. That is how Litex scales formal reasoning: making it accessible to more people, applicable to more complex problems, and usable by large-scale AI systems. The comparision between Litex and Lean is on our website(https://litexlang.com https://litexlang.com). There is also a straightforward tutorial about it on our web that you do not want to miss. Contact me if you are interested! Really hope we can scale formal reasoning in AI era together!

JonChesterfield 1y ago
The website tells me it's simple over and over but not what it is. What're the semantics? Which mathematical system is this? What can it prove?
- litexlang 1y ago
  Thank you Jon, I will put the semantics and the mathematical system behind online soon! Just give me some time!
thaumasiotes 1y ago
> Even Kids can formalize the multivariate equation in Litex in 2 minutes, while it [takes] an experienced expert hours of work in Lean 4. Well, I propose an alternative proof in lean4: import Mathlib.Tactic example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by have hy : y = 6 := by linear_combination 2 * h₁ - h₂ have hx : x = -4 := by -- you'd think h₁ - 3 * hy would work, but it won't linear_combination 1/2 * h₁ - 3/2 * hy exact ⟨hx, hy⟩ --- One thing I like about the lean proof, as opposed to the litex proof, is that it specifies why the steps are correct. If litex's strategy is "you describe the steps you want to take, and litex will automatically figure out why they're correct", how are you supposed to do any nontrivial proofs?
- c0balt 1y ago
  > how are you supposed to do any nontrivial proofs? One should also take a look at Isabelle/HOLs AFP here. You can get very far with Metis et al but it is very inefficient computationally. Especially when proofs get larger and/or layer on abstractions (proving something nontrivial likely involves building on existing algorithms etc.) the ability to make proofs efficient to verify is important.
- litexlang 1y ago
  Thank you thau! Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. We are comparing Lean and Litex under conditions where they don’t rely too much on external packages, which makes the comparison a bit fairer. (since Lean does have a very rich set of libraries, but building libraries is itself a challenge. Litex really needs to learn from Lean on how to build a successful library!).)(afterall, Litex can also abstract all proofs here and give it a name linear_combination, right?)
  - thaumasiotes 1y ago
    > Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. I learned about the `linear_combination` tactic from your example. Other than that, I use `have` and `exact`, which (a) are not advanced, and (b) are also used in your example. Before that, my first attempt at the lean proof looked like this: example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by -- double h₁ to cancel the x term have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁] conv at h₃ => ring_nf -- "ring normal form" -- subtract h₂ from h₃ have h₄ : (x * 4 + y * 6) - (4 * x + 5 * y) = 20 - 14 := by rw [h₂, h₃] conv at h₄ => ring_nf conv at h₁ => -- substitute y = 6 into h₁ rw [h₄] ring_nf -- solve for x have h₅ : ((18 + x * 2) - 18) / 2 = (10 - 18) / 2 := by rw [h₁] conv at h₅ => ring_nf apply And.intro h₅ h₄ > We are comparing Lean and Litex under conditions where they don’t rely too much on external packages This proof does have the advantage of not needing to import Mathlib.Tactic. Although again, that's something your proof does.

JonChesterfield 1y ago

The website tells me it's simple over and over but not what it is. What're the semantics? Which mathematical system is this? What can it prove?

litexlang 1y ago
Thank you Jon, I will put the semantics and the mathematical system behind online soon! Just give me some time!

thaumasiotes 1y ago

> Even Kids can formalize the multivariate equation in Litex in 2 minutes, while it [takes] an experienced expert hours of work in Lean 4. Well, I propose an alternative proof in lean4: import Mathlib.Tactic example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by have hy : y = 6 := by linear_combination 2 * h₁ - h₂ have hx : x = -4 := by -- you'd think h₁ - 3 * hy would work, but it won't linear_combination 1/2 * h₁ - 3/2 * hy exact ⟨hx, hy⟩ --- One thing I like about the lean proof, as opposed to the litex proof, is that it specifies why the steps are correct. If litex's strategy is "you describe the steps you want to take, and litex will automatically figure out why they're correct", how are you supposed to do any nontrivial proofs?

c0balt 1y ago
> how are you supposed to do any nontrivial proofs? One should also take a look at Isabelle/HOLs AFP here. You can get very far with Metis et al but it is very inefficient computationally. Especially when proofs get larger and/or layer on abstractions (proving something nontrivial likely involves building on existing algorithms etc.) the ability to make proofs efficient to verify is important.
litexlang 1y ago
Thank you thau! Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. We are comparing Lean and Litex under conditions where they don’t rely too much on external packages, which makes the comparison a bit fairer. (since Lean does have a very rich set of libraries, but building libraries is itself a challenge. Litex really needs to learn from Lean on how to build a successful library!).)(afterall, Litex can also abstract all proofs here and give it a name linear_combination, right?)
- thaumasiotes 1y ago
  > Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. I learned about the `linear_combination` tactic from your example. Other than that, I use `have` and `exact`, which (a) are not advanced, and (b) are also used in your example. Before that, my first attempt at the lean proof looked like this: example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by -- double h₁ to cancel the x term have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁] conv at h₃ => ring_nf -- "ring normal form" -- subtract h₂ from h₃ have h₄ : (x * 4 + y * 6) - (4 * x + 5 * y) = 20 - 14 := by rw [h₂, h₃] conv at h₄ => ring_nf conv at h₁ => -- substitute y = 6 into h₁ rw [h₄] ring_nf -- solve for x have h₅ : ((18 + x * 2) - 18) / 2 = (10 - 18) / 2 := by rw [h₁] conv at h₅ => ring_nf apply And.intro h₅ h₄ > We are comparing Lean and Litex under conditions where they don’t rely too much on external packages This proof does have the advantage of not needing to import Mathlib.Tactic. Although again, that's something your proof does.