Abstract
Recently, the use of computer-aided approaches such as formal verification of theorems and theorem discovery in economic studies has been developed. Most of the works are made for social choice theory in discrete domains, and it is said that these computer-aided techniques are not applicable for microeconomic problems in continuous domains, such as general equilibrium theory. In this work, it is proposed to enable computer-aided approaches to perform on microeconomic problems in continuous domains by including ”heuristics” to ease the complexity. With ”heuristics” axioms, it is shown that a special case of the first fundamental theorem of welfare economics is formally verified, and conditions where market failure does not occur despite of externalities.