Question: how to find posint solution of a specified equation?

Hi! how to find posint solution of this equation?

Is factorial move fast so that cannot solve?

any advice is appreciated.

restart

NULL

eq := `assuming`([factorial(x)+1 = y^2], [x::posint, y::posint])

factorial(x)+1 = y^2

(1)

`assuming`([solve(eq, {x, y})], [x <= 100, y <= 100])

{x = RootOf(factorial(_Z)-y^2+1), y = y}

(2)
 

NULL

Download find_posint_.mw

Please Wait...