# Zulip Chat Archive

## Stream: general

### Topic: linarith?

#### Bolton Bailey (Aug 22 2022 at 19:37):

Another thread was asking about how to see exactly what linarith is doing (`show_term`

is too verbose to be useful). I was thinking about this in the context of the relatively new tactic `linear_combination`

. It seems to me that just as `linear_combination`

proves an equality by way of a formal sum of known equalities, `linarith`

proves an inequality as a formal sum of known inequalities. What would it take to add a `linarith?`

tactic that outputs a `try this : linear_combination ...`

call? Is `linear_combination`

designed to work with inequalities? If not, could it be modified to do so?

#### Mario Carneiro (Aug 22 2022 at 22:32):

There is no tactic that can currently handle proofs by linear certificate

#### Eric Wieser (Dec 08 2022 at 01:30):

`polyrith`

produces the type of proof that `linear_combination`

can use

Last updated: Aug 03 2023 at 10:10 UTC