Inom formell talteori är en Gödelnumrering en funktion som tilldelar varje symbol och formel i ett formellt språk ett unikt naturligt tal som kallas Gödelnummer (GN). Begreppet användes för första gången av Kurt Gödel för att bevisa sin ofullständighetssats.
En Gödel-nummering kan tolkas som en kodning där varje symbol i en matematisk notation tilldelas ett nummer, och en ström av naturliga tal kan då representera någon form eller funktion. En numrering av mängden beräkningsbara funktioner kan då representeras av en ström av Gödel-nummer (även kallade effektiva nummer). Rogers ekvivalenssats anger kriterier för vilka numreringar av mängden beräkningsbara funktioner som är Gödel-nummer.