paper on computer-assisted math

Stream: general

[Steven Clontz]

Database_Driven_Mathematical_Inquiry-1.pdf (updated 04-08)

I'm a novice Lean user, so I'd appreciate feedback from this community on the formal mathematics content of the attached preprint (along with any other feedback you have, of course). Thanks!

[Eric Wieser]

(in Lean’s mathlib, one might apply the theorems add_assoc and mul_comm), the single Lean tactic simp alternatively handles this proof in just four characters: of course one expression simplifies to the other

Unfortunately neither of these statements are true; you need rw not apply, and simp does not solve problems with associativity and commutativity. ring is the right choice of four characters.

[Steven Clontz]

Ha, that's what I get working from memory, thank you!

[Steven Clontz]

Now updated:

While one might accomplish this through applications of
associativity and commutativity (in Lean's \texttt{mathlib}, one might
\verb|rewrite| this goal using the theorems \verb|add_assoc| and \verb|mul_comm|),
the single Lean tactic \verb|ring| alternatively
handles this proof in just four characters: \textit{of course} the
usual properties of \verb|ring|s show that these expressions
are equal to the other.