Auto-formalized versions of GSM8K and MATH500 auto-formalized and filtered with Goedel models