Combining Lean with Symbolic Computation to Resolve Matching

Stream: new members

[ByronW]

Is there any way to combine Lean4 with symbolic computation? One challenge I've encountered is the mismatch between Lean's logic, which operates on propositions, and the intricacies of symbolic computations. Specifically, situations arise where expressions like "(1/a>0):Prop" and "(1/a>0*2):Prop" mismatch as expected, leading to frustration and confusion.

[Martin Dvořák]

There is https://robertylewis.com/leanmm/ but nobody maintains it afaik.

[Martin Dvořák]

For these kinds of problems, I'd rather advice you to learn how to prove that one implies the other.

[ByronW]

Martin Dvořák said:

For these kinds of problems, I'd rather advice you to learn how to prove that one implies the other.

Thanks. I know this project. And the two propositions match through theorems like "a>b->b=c->a>c". However, my aim is to explore more efficient and automated approaches to address these types of problems. Ideally, I'm looking for a built-in package or functionality in Lean that can seamlessly handle these types of matching issues.

[Martin Dvořák]

We kinda have. Often you can use the tactic convert or something like that.

[ByronW]

Martin Dvořák said:

We kinda have. Often you can use the tactic convert or something like that.

Thank you, this indeed proves it. What if I want to use the prop as a hypothesis for a theorem? For example, look at
theorem am_gm2 {x y:ℝ}(ha:x≥0)(hb:y≥0):x+y≥2*Real.sqrt (x*y):=by sorry. Then there is a type mismatch in"am_gm2 p1 p2 --(p1:1/b>=0),(p2:(1/a)*2>=0*2)"

[Kevin Buzzard]

Use ` to enclose code, or else Zulip markdown mangles everything with a * in (you can edit your post). For more information see #backticks

[Martin Dvořák]

ByronW said:

What if I want to use the prop as a hypothesis for a theorem?

Please post a #mwe of a situation where convert does not do the job for you. I'll try to find a workaround.