# When Reduce yields False for a system of inequalities, can I take this as a formal proof? [closed]

As part of the proof of a proposition in an economics paper, I need to show that a system of inequalities in four variables is inconsistent. Because the system is complicated, I cannot show this analytically. However, Reduce[System,{x1, x2, x3, x4}, Reals] returns False. Is it acceptable to use this result as part of the formal proof of my proposition? That is, is the algorithm that Reduce uses exact? Or does it use short-cuts, approximations, etc.?

• It is certainly a verification if you accept that Reduce has no bugs that are affecting its evaluation of your inequalities. Whether or not citing the results in a paper will be accepted, is a something the journal editor will decide. It is not an issue for this site. – m_goldberg Jul 20 '17 at 15:04

In general, no... Mathematica has bugs and problems with differences between its interpretation of things vs. what users may expect. A better approach would be to post the equations or describe them to see what form they take and find out if anyone knows a way to prove they're inconsistent. For instance, it's entirely possible someone may know what algorithm Reduce will use to prove your inequalities, and you may be able to reproduce what it does in more straightforwardly provable steps.